donovancrichton

{-
data Λ : List Type -> Type where
  Var : (xs : List Type) -> Λ xs
  Lam : Λ (x :: xs) -> Λ xs
  App : Λ xs -> Λ xs -> Λ xs
-}

Scoped : Type -> Type
Scoped i = i -> List i -> Type

donovancrichton

f : (n : Nat) -> n = n + 0
f 0 = Refl
f (S k) = 
  let ih : k = plus k 0
      ih = f k
  in rewrite sym ih in Refl

donovancrichton

%default total
ℕ : Type
ℕ = Nat

data D : ℕ -> Type where
  K0 : D Z
  K1 : {k : ℕ} -> D k -> D (S k)
  K2 : {k : ℕ} -> D k -> D Z

data Ctx : ℕ -> Type where

donovancrichton

-- Example 3.8 from Hanmana and Fiore - page 63
-- (Foundations of GADTS and Inductive Families)

data Expr : Type -> Type where
  Const : Int -> Expr Int
  IsZero : Expr Int -> Expr Bool
  If : Expr Bool -> Expr a -> Expr a -> Expr a

-- Page 66: Context specialised for the Expr type above
--   General form for non-root cases is:

donovancrichton

data MyList : Type -> Type where
  Nil : {a : Type} -> MyList a
  (::) : {a : Type} -> a -> MyList a -> MyList a

f : MyList b -> ()
f [] = ()
f ((::) {a} x xs) = ?normal

g : MyList b -> ()
g [] = ()

donovancrichton

%default total
data MyList : Type -> Type where
  Nil : {a : Type} -> MyList a
  (::) : {a : Type} -> a -> MyList a -> MyList a

F : MyList a -> Maybe Type
F [] = Nothing
F ((::) {a} x xs) = Just a

G : MyList a -> Maybe Type

donovancrichton

data MyList : Type -> Type where
  Nil : {a : Type} -> MyList a
  (::) : {a : Type} -> a -> MyList a -> MyList a

f : MyList a -> ()
f [] = ()
f (x :: xs) = ?normal

g : MyList a -> ()
g [] = ()

donovancrichton

%default total 
data Term : Type -> Type where
  Const : {a : Type} -> a -> Term a
  Pair : {a : Type} -> {b : Type} -> Term a -> Term b -> Term (a, b)
  App : {a : Type} -> {b : Type} -> Term (a -> b) -> Term a -> Term b

GoLeft : {a : Type} -> Term a -> Maybe Type
GoLeft (Const x) = Nothing
GoLeft (Pair {a} x y) = Just a
GoLeft (App {a} {b} f x) = Just (a -> b)

donovancrichton

data ParamType = OptionParams
               | FlagParams
               | ArgParams
               | CmdParams

data Visibility = Visible
                | Hidden
                | Internal

donovancrichton

--module Queue
 
import Syntax.WithProof
 
%default total
   
data State = Empty | NonEmpty
 
Eq State where
  Empty == Empty = True