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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.InstanceArguments

Synopsis

- findInstance :: MetaId -> Maybe [Candidate] -> TCM ()
- isInstanceConstraint :: Constraint -> Bool
- shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool
- postponeInstanceConstraints :: TCM a -> TCM a

# Documentation

findInstance :: MetaId -> Maybe [Candidate] -> TCM () Source #

`findInstance m (v,a)s` tries to instantiate on of the types `a`s of the candidate terms `v`s to the type `t` of the metavariable `m`. If successful, meta `m` is solved with the instantiation of `v`. If unsuccessful, the constraint is regenerated, with possibly reduced candidate set. The list of candidates is equal to `Nothing` when the type of the meta wasn't known when the constraint was generated. In that case, try to find its type again.

isInstanceConstraint :: Constraint -> Bool Source #

shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool Source #

postponeInstanceConstraints :: TCM a -> TCM a Source #