Idris2Doc : Language.Reflection

Language.Reflection

dataElab : 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 : FC -> String -> Elaba
LogMsg : String -> Nat -> String -> Elab ()
LogTerm : String -> Nat -> String -> TTImp -> Elab ()
Check : TTImp -> Elabexpected
Quote : (0 _ : 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 -> Elab ()
check : TTImp -> Elabexpected
  Check that some TTImp syntax has the expected type
Returns the type checked value

Totality: total
declare : ListDecl -> Elab ()
  Make some top level declarations

Totality: total
fail : String -> Elaba
  Report an error in elaboration

Totality: total
failAt : FC -> String -> Elaba
Totality: total
genSym : String -> ElabName
  Generate a new unique name

Totality: total
getCons : Name -> Elab (ListName)
  Get the constructors of a fully qualified data type name

Totality: total
getLocalType : Name -> ElabTTImp
  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 (MaybeTTImp)
  Get the goal type of the current elaboration

Totality: total
inCurrentNS : Name -> ElabName
  Given a name, return the name decorated with the current namespace

Totality: total
lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (tyval)) -> Elab ((val : x) -> tyval)
  Build a lambda expression

Totality: total
localVars : Elab (ListName)
  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) -> ElabTTImp
  Return TTImp syntax of a given value

Totality: total