idris-1.3.2: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Elab.Implementation

Description

 

Documentation

elabImplementation Source #

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 ()