Idris2Doc : TTImp.Elab.As

TTImp.Elab.As

(source)

Definitions

checkAs : RefCtxtDefs=>RefMDMetadata=>RefUSTUState=>RefEST (EStatevars) =>RefSynSyntaxInfo=>RefROptsREPLOpts=>RigCount->ElabInfo->NestedNamesvars->EnvTermvars->FC->FC->UseSide->Name->RawImp->Maybe (Gluedvars) ->Core (Termvars, Gluedvars)
Visibility: export