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]

david-christiansen

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 [

david-christiansen

data Typ =
    IntTyp
  | BolTyp
  | FunTyp Typ Typ

toType : Typ -> Type
toType IntTyp       = Integer
toType BolTyp       = Bool
toType (FunTyp x y) = toType x -> toType y

david-christiansen

module NotElem

import Language.Reflection.Elab
import Language.Reflection.Utils

import Data.List


emptyNotElem : {a : Type} -> {x : a} -> Elem x [] -> Void
emptyNotElem Here impossible

david-christiansen

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

david-christiansen

module ClassNonsense

import Language.Reflection.Elab

class Foo t where
  constructor MkFoo
  foo : t

myFoo : Foo Nat
myFoo = MkFoo 1