| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Int | this many implicits have to be inserted
BadImplicits | hidden argument where there should have been a non-hidden arg
NoSuchName String | bad named argument
NoInsertNeeded |

Instances

Show ImplicitInsertion

impInsert :: Int -> ImplicitInsertion | Source

insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertion | Source

The list should be non-empty.
Produced by Haddock version 2.4.2