Idris2Doc : TTImp.Interactive.Intro

TTImp.Interactive.Intro

(source)

Definitions

intro : RefCtxtDefs=>RefSynSyntaxInfo=>RefMDMetadata=>RefUSTUState=>RefROptsREPLOpts=>Int->Name->EnvTermlhsCtxt->TermlhsCtxt->Core (ListIRawImp)
Visibility: export