View difference between Paste ID: cVXLmbzD and kthpU2c0

 import Data.Vect
 
 ||| Constant Types
 data ANTConst = I Int | BI Integer | Fl Double | Ch Char | Str String
 
   ||| Context
   ||| @n total number of vars
   data ANTContext : {n : Nat} -> Type
   data Expr : ANTContext -> Type
 
   data ANTContext : {n : Nat} -> Type where
     AddVar : (ctx : ANTContext {n}) -> Expr ctx -> ANTContext {n=(S n)}
 
   getExpr : (ctx : ANTContext) -> Fin n -> Expr ctx
   getExpr (AddVar c e) 0 = e
   getExpr (AddVar c e) (S n) = getExpr c n
 
   betaEq : Expr ctx -> Expr ctx -> Type
   betaEq = ?x
 
   ||| This represents when a context implies something. It is laid out
   ||| as the basic rules of the type theory system
   ||| Taken from https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf page 11
   data Expr : ANTContext -> Type where
     |||     G |- f : (x : S) -> T   G |- s : S
     ||| App ----------------------------------
     |||     G |- f s : T[s/x]
     App : (ctx : ANTContext {n})
       -> (fInd : Fin n)
       -> (sInd : Fin n)
       -> ?betaEq (getExpr ctx fInd) (getExpr ctx sInd)
       -> Expr ctx
     |||     G;\x:S |- e : T   G |- (x : S) -> T : Type(n)
     ||| Lam ---------------------------------------------
     |||     G |- \x:S.e : (x : S) -> T
     ||| Given a context, an arg type within that context, and an expression
     ||| that uses that var, returns a Lam (variable name not specified
     ||| since we are using DeBrujin indexes)
     Lam : (ctx : ANTContext) -> (argType : Expr ctx)
       -> Expr (AddVar ctx argType) -> Expr ctx