Idris2Doc : TTImp.Interactive.MakeLemma

TTImp.Interactive.MakeLemma

(source)

Definitions

makeLemma : RefCtxtDefs=>RefSynSyntaxInfo=>FC->Name->Nat->ClosedTerm->Core (RawImp, RawImp)
Visibility: export