Idris2Doc : TTImp.Interactive.MakeLemma

TTImp.Interactive.MakeLemma

(source)

Definitions

makeLemma : Ref Ctxt Defs => Ref Syn SyntaxInfo => FC -> Name -> Nat -> ClosedTerm -> Core (RawImp, RawImp)
Visibility: export