idris-0.10.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Elab.Record

Synopsis

Documentation

elabRecord Source

Arguments

:: ElabInfo 
-> ElabWhat 
-> Docstring (Either Err PTerm)

The documentation for the whole declaration

-> SyntaxInfo 
-> FC 
-> DataOpts 
-> Name

The name of the type being defined

-> FC

The precise source location of the tycon name

-> [(Name, FC, Plicity, PTerm)]

Parameters

-> [(Name, Docstring (Either Err PTerm))]

Parameter Docs

-> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]

Fields

-> Maybe (Name, FC)

Constructor Name

-> Docstring (Either Err PTerm)

Constructor Doc

-> SyntaxInfo

Constructor SyntaxInfo

-> Idris () 

Elaborate a record declaration