Idris.Desugar

Definitions

data Side : Type

Totality: total
Visibility: public export
Constructors:

LHS : Side

AnyExpr : Side

Hint: 

Eq Side

extendSyn : Ref Syn SyntaxInfo => Ref Ctxt Defs => SyntaxInfo -> Core ()

Visibility: export

desugarFnOpt : Ref Syn SyntaxInfo => Ref Ctxt Defs => Ref UST UState => Ref MD Metadata => Ref ROpts REPLOpts => List Name -> PFnOpt -> Core FnOpt

Visibility: export

desugarDecl : Ref Syn SyntaxInfo => Ref Ctxt Defs => Ref UST UState => Ref MD Metadata => Ref ROpts REPLOpts => List Name -> PDecl -> Core (List ImpDecl)

Visibility: export

desugarDo : Ref Syn SyntaxInfo => Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref ROpts REPLOpts => Side -> List Name -> Maybe Namespace -> PTerm -> Core RawImp

Visibility: export

desugar : Ref Syn SyntaxInfo => Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref ROpts REPLOpts => Side -> List Name -> PTerm -> Core RawImp

Visibility: export