Agda-2.2.10: A dependently typed functional programming language and proof assistant

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

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

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

The list should be non-empty.