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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Implicit

Description

Functions for inserting implicit arguments at the right places.

Synopsis

- implicitArgs :: Int -> (Hiding -> Bool) -> Type -> TCM (Args, Type)
- implicitNamedArgs :: Int -> (Hiding -> ArgName -> Bool) -> Type -> TCM (NamedArgs, Type)
- newMetaArg :: ArgInfo -> ArgName -> Type -> TCM (MetaId, Term)
- newInteractionMetaArg :: ArgInfo -> ArgName -> Type -> TCM (MetaId, Term)
- data ImplicitInsertion
  - = ImpInsert [Hiding]
  - | BadImplicits
  - | NoSuchName ArgName
- pattern NoInsertNeeded :: ImplicitInsertion
- insertImplicit :: NamedArg e -> [Dom a] -> ImplicitInsertion
- insertImplicit' :: NamedArg e -> [Arg ArgName] -> ImplicitInsertion

# Documentation

implicitArgs Source #

Arguments

:: Int | `n`, the maximum number of implicts to be inserted.
-> (Hiding -> Bool) | `expand`, the predicate to test whether we should keep inserting.
-> Type | The (function) type `t` we are eliminating.
-> TCM (Args, Type) | The eliminating arguments and the remaining type.

`implicitArgs n expand t` generates up to `n` implicit arguments metas (unbounded if `n<0`), as long as `t` is a function type and `expand` holds on the hiding info of its domain.

implicitNamedArgs Source #

Arguments

:: Int | `n`, the maximum number of implicts to be inserted.
-> (Hiding -> ArgName -> Bool) | `expand`, the predicate to test whether we should keep inserting.
-> Type | The (function) type `t` we are eliminating.
-> TCM (NamedArgs, Type) | The eliminating arguments and the remaining type.

`implicitNamedArgs n expand t` generates up to `n` named implicit arguments metas (unbounded if `n<0`), as long as `t` is a function type and `expand` holds on the hiding and name info of its domain.

newMetaArg Source #

Arguments

:: ArgInfo | Kind/relevance of meta.
-> ArgName | Name suggestion for meta.
-> Type | Type of meta.
-> TCM (MetaId, Term) | The created meta as id and as term.

Create a metavariable according to the `Hiding` info.

newInteractionMetaArg Source #

Arguments

:: ArgInfo | Kind/relevance of meta.
-> ArgName | Name suggestion for meta.
-> Type | Type of meta.
-> TCM (MetaId, Term) | The created meta as id and as term.

Create a questionmark according to the `Hiding` info.

data ImplicitInsertion Source #

Possible results of `insertImplicit`.

Constructors

ImpInsert [Hiding] | Success: this many implicits have to be inserted (list can be empty).
BadImplicits | Error: hidden argument where there should have been a non-hidden argument.
NoSuchName ArgName | Error: bad named argument.

Instances

Show ImplicitInsertion Source # |
Instance details Defined in Agda.TypeChecking.Implicit Methods showsPrec :: Int -> ImplicitInsertion -> ShowS Source # show :: ImplicitInsertion -> String Source # showList :: [ImplicitInsertion] -> ShowS Source #

pattern NoInsertNeeded :: ImplicitInsertion Source #

insertImplicit Source #

Arguments

:: NamedArg e | Next given argument `a`.
-> [Dom a] | Expected arguments `ts`.
-> ImplicitInsertion |

If the next given argument is `a` and the expected arguments are `ts` `insertImplicit' a ts` returns the prefix of `ts` that precedes `a`.

If `a` is named but this name does not appear in `ts`, the `NoSuchName` exception is thrown.

insertImplicit' Source #

Arguments

:: NamedArg e | Next given argument `a`.
-> [Arg ArgName] | Expected arguments `ts`.
-> ImplicitInsertion |

If the next given argument is `a` and the expected arguments are `ts` `insertImplicit' a ts` returns the prefix of `ts` that precedes `a`.

If `a` is named but this name does not appear in `ts`, the `NoSuchName` exception is thrown.