Skip to content

Instantly share code, notes, and snippets.

Avatar

David Thrane Christiansen david-christiansen

View GitHub Profile
@david-christiansen
david-christiansen / Addition.idr
Created Aug 2, 2013
Using type classes for logic programming
View Addition.idr
module Addition
class Plus (n : Nat) (m : Nat) (o : Nat) where {}
instance Plus Z m m where {}
instance Plus n m o => Plus (S n) m (S o) where {}
parameters (n : Nat, m : Nat)
@david-christiansen
david-christiansen / Lambda.idr
Created Jul 29, 2013
Error with idiom brackets in equality type
View Lambda.idr
module Lambda
%default total
infixr 8 ==>
data T : Type where
U : T
NAT : T
(*) : T -> T -> T
View gist:4994631
module PropDemo
data GreaterThanTwo : Nat -> Type where
threeOK : GreaterThanTwo 3
moreOK : GreaterThanTwo n -> GreaterThanTwo (S n)
total sumGreater : GreaterThanTwo n -> GreaterThanTwo m -> GreaterThanTwo (n + m)
sumGreater threeOK mOK = moreOK (moreOK (moreOK mOK))
sumGreater (moreOK nOK') mOK = moreOK (sumGreater nOK' mOK)
View gist:4994451
module HList
%default total
data HList : List Type -> Type where
(::) : t -> (xs : HList ts) -> HList (t :: ts)
Nil : HList []
foo : HList [Int, String, Int]
foo = [3, "yes", 17]
View MTac.idr
syntax mmatch [t] as {x} returning [ty] cases [cs] =
Match (\x => ty) t cs
syntax pat {x} "." [tm] = PTele (\x => tm)
syntax [tm1] "=>" [tm2] = PBase tm1 tm2
foo : Tac (List ())
foo = mmatch Z as y returning (List ())
cases [
View STLC.idr
data Typ =
IntTyp
| BolTyp
| FunTyp Typ Typ
toType : Typ -> Type
toType IntTyp = Integer
toType BolTyp = Bool
toType (FunTyp x y) = toType x -> toType y
View NotElem.idr
module NotElem
import Language.Reflection.Elab
import Language.Reflection.Utils
import Data.List
emptyNotElem : {a : Type} -> {x : a} -> Elem x [] -> Void
emptyNotElem Here impossible
View Schema.idr
data HList : List Type -> Type where
Nil : HList []
(::) : t -> HList ts -> HList (t :: ts)
%name HList xs,ys
append : HList ts -> HList ts' -> HList (ts ++ ts')
append [] ys = ys
append (x :: xs) ys = x :: append xs ys
View ClassNonsense.idr
module ClassNonsense
import Language.Reflection.Elab
class Foo t where
constructor MkFoo
foo : t
myFoo : Foo Nat
myFoo = MkFoo 1
View ClassNonsense.idr
module ClassNonsense
import Language.Reflection.Elab
class Foo a where
foo : a -> () -> a
class Foo a => Bar a where
constructor MkFoo
bar : a -> Int