TTImp.Unelab

Definitions

data UnelabMode : Type

Totality: total
Visibility: public export
Constructors:

Full : UnelabMode

NoSugar : Bool -> UnelabMode

ImplicitHoles : UnelabMode

Hint: 

Eq UnelabMode

unelabNoSugar : Ref Ctxt Defs => Env Term vars -> Term vars -> Core IRawImp

Visibility: export

unelabUniqueBinders : Ref Ctxt Defs => Env Term vars -> Term vars -> Core IRawImp

Visibility: export

unelabNoPatvars : Ref Ctxt Defs => Env Term vars -> Term vars -> Core IRawImp

Visibility: export

unelabNest : Ref Ctxt Defs => UnelabMode -> List (Name, Nat) -> Env Term vars -> Term vars -> Core IRawImp

Visibility: export

unelab : Ref Ctxt Defs => Env Term vars -> Term vars -> Core IRawImp

Visibility: export