HORIZON HASKELLDocslts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K
Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Free.Reduce

Free variable check that reduces the subject to make certain variables not free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.

Synopsis
  • PackageAgda-2.8.0.2
  • Exports4
  • LanguageHaskell2010
  • LicenceMIT
  • SourceReduce.hs
classclass (PrecomputeFreeVars a, Subst a) => ForceNotFree a where
#
Instances10ForceNotFree, …
valueforceNotFree
  1. :: (ForceNotFree a, Reduce a, MonadReduce m)
  2. => IntSet
  3. -> a
  4. -> m (IntMap IsFree, a)
Source#

Try to enforce a set of variables not occurring in a given type. Returns a possibly reduced version of the type and for each of the given variables whether it is either not free, or maybe free depending on some metavariables.

valuereallyFree
  1. :: (MonadReduce m, Reduce a, ForceNotFree a)
  2. => IntSet
  3. -> a
  4. -> m (Either Blocked_ (Maybe a))
Source#

Checks if the given term contains any free variables that are in the given set of variables, possibly reducing the term in the process. Returns `Right Nothing` if there are such variables, `Right (Just v')` if there are none (where v' is the possibly reduced version of the given term) or `Left b` if the problem is blocked on a meta.

datadata IsFree
Source#

A variable can either not occur (NotFree) or it does occur (MaybeFree). In the latter case, the occurrence may disappear depending on the instantiation of some set of metas.

Constructors

Instances2Eq, Show
  • Eq IsFreeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Reduce
  • Show IsFreeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Reduce