TTImp.Elab.Case

Definitions

changeVar : Var vs -> Var vs -> Term vs -> Term vs

Visibility: export

caseBlock : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => RigCount -> ElabInfo -> FC -> NestedNames vars -> Env Term vars -> List FnOpt -> RawImp -> Term vars -> Term vars -> RigCount -> List ImpClause -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export

checkCase : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => RigCount -> ElabInfo -> NestedNames vars -> Env Term vars -> FC -> List FnOpt -> RawImp -> RawImp -> List ImpClause -> Maybe (Glued vars) -> Core (Term vars, Glued vars)

Visibility: export