Idris2Doc : Core.Context.Data

Core.Context.Data

(source)

Definitions

addData : RefCtxtDefs=>Scope->Visibility->Int->DataDef->CoreInt
Visibility: export