Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Implicit
Description
Functions for inserting implicit arguments at the right places.
Synopsis
data ImplicitInsertion
= ImpInsert Int
| BadImplicits
| NoSuchName String
| NoInsertNeeded
impInsert :: Int -> ImplicitInsertion
insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertion
Documentation
data ImplicitInsertion Source
Constructors
ImpInsert Intthis many implicits have to be inserted
BadImplicitshidden argument where there should have been a non-hidden arg
NoSuchName Stringbad named argument
NoInsertNeeded
impInsert :: Int -> ImplicitInsertionSource
insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertionSource
The list should be non-empty.
Produced by Haddock version 2.6.0