Core.Case.CaseBuilder

Definitions

data Phase : Type

Totality: total
Visibility: public export
Constructors:

CompileTime : RigCount -> Phase

RunTime : Phase

Hint: 

Eq Phase

mkPat : Ref Ctxt Defs => Bool -> List Pat -> ClosedTerm -> ClosedTerm -> Core Pat

Visibility: export

argToPat : Ref Ctxt Defs => ClosedTerm -> Core Pat

Visibility: export

patCompile : Ref Ctxt Defs => FC -> Name -> Phase -> ClosedTerm -> List01 True (List Pat, ClosedTerm) -> Core (args : List Name ** CaseTree args)

Visibility: export

simpleCase : Ref Ctxt Defs => FC -> Phase -> Name -> ClosedTerm -> List01 True (ClosedTerm, ClosedTerm) -> Core (args : List Name ** CaseTree args)

Visibility: export

getPMDef : Ref Ctxt Defs => FC -> Phase -> Name -> ClosedTerm -> List Clause -> Core (args : List Name ** (CaseTree args, List Clause))

Visibility: export