Idris2Doc : Language.Mk

Language.Mk

(source)

Reexports

importpublic Language.Reflection

Definitions

getMk' : ty->Elab (FC, Name)
Totality: total
Visibility: export
getMk : ty->ElabName
Totality: total
Visibility: export
Mk : ty->Elaba
Totality: total
Visibility: export