- data Elab : Type -> Type
Elaboration scripts
Where types/terms are returned, binders will have unique, if not
necessarily human readabe, names
Totality: total
Constructors:
- Pure : a -> Elab a
- Bind : Elab a -> (a -> Elab b) -> Elab b
- Fail : FC -> String -> Elab a
- LogMsg : String -> Nat -> String -> Elab ()
- LogTerm : String -> Nat -> String -> TTImp -> Elab ()
- Check : TTImp -> Elab expected
- Quote : (0 _ : val) -> Elab TTImp
- Lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> ty val)
- Goal : Elab (Maybe TTImp)
- LocalVars : Elab (List Name)
- GenSym : String -> Elab Name
- InCurrentNS : Name -> Elab Name
- GetType : Name -> Elab (List (Name, TTImp))
- GetLocalType : Name -> Elab TTImp
- GetCons : Name -> Elab (List Name)
- Declare : List Decl -> Elab ()
- check : TTImp -> Elab expected
Check that some TTImp syntax has the expected type
Returns the type checked value
Totality: total- declare : List Decl -> Elab ()
Make some top level declarations
Totality: total- fail : String -> Elab a
Report an error in elaboration
Totality: total- failAt : FC -> String -> Elab a
- Totality: total
- genSym : String -> Elab Name
Generate a new unique name
Totality: total- getCons : Name -> Elab (List Name)
Get the constructors of a fully qualified data type name
Totality: total- getLocalType : Name -> Elab TTImp
Get the type of a local variable
Totality: total- getType : Name -> Elab (List (Name, TTImp))
Given a possibly ambiguous name, get all the matching names and their types
Totality: total- goal : Elab (Maybe TTImp)
Get the goal type of the current elaboration
Totality: total- inCurrentNS : Name -> Elab Name
Given a name, return the name decorated with the current namespace
Totality: total- lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> ty val)
Build a lambda expression
Totality: total- localVars : Elab (List Name)
Get the names of the local variables in scope
Totality: total- logGoal : String -> Nat -> String -> Elab ()
Log the current goal type, if the log level is >= the given level
Totality: total- logMsg : String -> Nat -> String -> Elab ()
Write a log message, if the log level is >= the given level
Totality: total- logTerm : String -> Nat -> String -> TTImp -> Elab ()
Write a log message and a rendered term, if the log level is >= the given level
Totality: total- quote : (0 _ : val) -> Elab TTImp
Return TTImp syntax of a given value
Totality: total