Idris2Doc : TTImp.ProcessRecord

TTImp.ProcessRecord

(source)

Definitions

processRecord : RefCtxtDefs=>RefMDMetadata=>RefUSTUState=>RefSynSyntaxInfo=>RefROptsREPLOpts=>ListElabOpt->NestedNamesvars->EnvTermvars->MaybeString->WithDefaultVisibilityPrivate->MaybeTotalReq->ImpRecord->Core ()
Visibility: export