Idris.Elab.Implementation

Documentation

elabImplementation

Arguments

:: ElabInfo

-> SyntaxInfo

-> Docstring (Either Err PTerm)

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

-> ElabWhat

phase

-> FC

-> [(Name, PTerm)]

constraints

-> [Name]

parent dictionary names (optionally)

-> Accessibility

-> FnOpts

-> Name

the interface

-> FC

precise location of interface name

-> [PTerm]

interface parameters (i.e. implementation)

-> [(Name, PTerm)]

Extra arguments in scope (e.g. implementation in where block)

-> PTerm

full implementation type

-> Maybe Name

explicit name

-> [PDecl]

-> Idris ()