kuribas

module Main
import Data.String
import Data.Maybe
import Data.List
import Data.List.Elem
import Data.Vect
import Records

interface HandlerImpl handler where
  handlerLabel : String

kuribas

Idris2 proofs of leftPad and fulcrum from the Great theorem prover showdown. https://www.hillelwayne.com/post/theorem-prover-showdown/

An attempt was made to make readable proofs which can be easily followed.

Some final observations:

• idris2 is not made for intrinsics proofs, even though it provides facilities for it. It can be felt in the way the standard library is organised. Some proofs are missing (proofs about Int, about

kuribas

import Data.List

infixr 1 =~
infixr 1 >~
infixr 1 =~<

(=~) : (a:k) -> {b:k} -> (a = b) -> (a = b)
(=~) _ prf = prf

qed : {a:k} -> (a = a)

kuribas

module Records
import Data.String
import Data.Maybe
import Data.List
import Data.List.Elem
import Data.Vect
import Data.Morphisms
import Decidable.Equality
import Data.IOArray.Prims

kuribas

module Main
import Data.String
import Data.Maybe
import Data.List
import Data.List.Elem
import Data.Vect
import Data.Morphisms
import Decidable.Equality

infixr 10 :->

kuribas

record Foo (f : Type -> Type) where
  constructor MkFoo
  baz : f Int
  bar : f String

Identity : Type -> Type    
Identity x = x

foo2 : Foo Identity
foo2 = MkFoo { baz = 9.3

kuribas

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

kuribas

{-# LANGUAGE GeneralizedNewtypeDeriving  #-}
module ValidationT where
import Data.Validation
import Data.Functor.Compose
import Control.Monad.IO.Class
import qualified Data.DList as DList
import Control.Monad.Except
import Data.These

-- | Applicative only validation transformer

kuribas

memoize2 :: (Eq a, Hashable a) => (a -> IO b) -> IO (a -> b)
memoize2 f = do
  ref <- newIORef HashMap.empty
  pure $ \x ->
    do mp <- readIORef ref
       case HashMap.lookup x mp of
         Nothing -> unsafePerformIO $ do
                       res <- f x
                       writeIORef ref $ HashMap.insert x res mp
                       pure res

kuribas

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Test where
import Data.Aeson
import Data.Aeson.Types
import Data.Text (Text)
import Data.Scientific
import Control.Monad
import Control.Applicative