Idris2Doc : Language.Reflection

Language.Reflection

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 -> Elaba
Bind : Elaba -> (a -> Elabb) -> Elabb
Fail : String -> Elaba
LogMsg : String -> Nat -> String -> ElabUnit
LogTerm : String -> Nat -> String -> TTImp -> ElabUnit
Check : TTImp -> Elabexpected
Quote : val -> ElabTTImp
Lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (tyval)) -> Elab ((val : x) -> tyval)
Goal : Elab (MaybeTTImp)
LocalVars : Elab (ListName)
GenSym : String -> ElabName
InCurrentNS : Name -> ElabName
GetType : Name -> Elab (List (Name, TTImp))
GetLocalType : Name -> ElabTTImp
GetCons : Name -> Elab (ListName)
Declare : ListDecl -> ElabUnit
check : TTImp -> Elabexpected
Check that some TTImp syntax has the expected type
Returns the type checked value
declare : ListDecl -> ElabUnit
Make some top level declarations
fail : String -> Elaba
Report an error in elaboration
genSym : String -> ElabName
Generate a new unique name
getCons : Name -> Elab (ListName)
Get the constructors of a fully qualified data type name
getLocalType : Name -> ElabTTImp
Get the type of a local variable
getType : Name -> Elab (List (Name, TTImp))
Given a possibly ambiguous name, get all the matching names and their types
goal : Elab (MaybeTTImp)
Get the goal type of the current elaboration
inCurrentNS : Name -> ElabName
Given a name, return the name decorated with the current namespace
lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (tyval)) -> Elab ((val : x) -> tyval)
Build a lambda expression
localVars : Elab (ListName)
Get the names of the local variables in scope
logGoal : String -> Nat -> String -> ElabUnit
Log the current goal type, if the log level is >= the given level
logMsg : String -> Nat -> String -> ElabUnit
Write a log message, if the log level is >= the given level
logTerm : String -> Nat -> String -> TTImp -> ElabUnit
Write a log message and a rendered term, if the log level is >= the given level
quote : val -> ElabTTImp
Return TTImp syntax of a given value