TTImp.Interactive.GenerateDef

Definitions

makeDefFromType : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => FC -> SearchOpts -> Name -> Nat -> ClosedTerm -> Core (Search (FC, List ImpClause))

Visibility: export

makeDef : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => (NonEmptyFC -> (Name, (Nat, ClosedTerm)) -> Bool) -> Name -> Core (Search (FC, List ImpClause))

Visibility: export

mostUsed : List ImpClause -> List ImpClause -> Ordering

Visibility: export

makeDefSort : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => (NonEmptyFC -> (Name, (Nat, ClosedTerm)) -> Bool) -> Nat -> (List ImpClause -> List ImpClause -> Ordering) -> Name -> Core (Search (FC, List ImpClause))

Visibility: export

makeDefN : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => (NonEmptyFC -> (Name, (Nat, ClosedTerm)) -> Bool) -> Nat -> Name -> Core (List (FC, List ImpClause))

Visibility: export