View difference between Paste ID: aJeFkfX9 and PeHAA8xx

-- + Errors (5)
+
- |-- z.idr line 12 col 10:
+
- |   When checking type of Main.getExpr:
+
- |   No such variable Expr
+
- |-- z.idr line 15 col 9:
+
- |   When checking type of Main.betaEq:
+
- |   No such variable Expr
+
- |-- z.idr line 13 col 2:
+
- |   No type declaration for Main.getExpr
+
- |-- z.idr line 16 col 2:
+
- |   No type declaration for Main.betaEq
+
- `-- z.idr line 28 col 17:
+
-     When checking type of Main.App:
+  data Expr : ANTContext -> Type
-     No such variable getExpr
+
   getExpr : ANTContext -> Fin n -> Expr ctx
---------------------- code below ------------------------
+
 
   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 ----------------------------------
-
+
     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