idris-0.9.14.3: Functional Programming Language with Dependent Types
Idris.Elab.Data
Synopsis
elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris () Source
^^ TODO: the above is a comment from the past; forcenames is probably no longer needed