david-christiansen

module Bugfind



import Language.Reflection
import Language.Reflection.Util

foo : TT
foo = Erased

david-christiansen

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

module Lambda

%default total

infixr 8 ==>

data T : Type where
  U : T
  NAT : T
  (*) : T -> T -> T

david-christiansen

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)

david-christiansen

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]