Agda

Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Conversion.Pure

Synopsis

pureConversion :: TCM b -> (Blocker -> TCM b) -> (a -> TCM b) -> TCM a -> TCM b
runPureConversion :: TCM a -> TCM a
pureEqualTerm :: Type -> Term -> Term -> TCM Bool
pureBlockOrEqualTerm :: Type -> Term -> Term -> TCM (Either Blocker Bool)
pureBlockOrEqualTermPureTCM :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool)
pureBlockOrEqualType :: Type -> Type -> TCM (Either Blocker Bool)
pureBlockOrEqualTypePureTCM :: PureTCM m => Type -> Type -> m (Either Blocker Bool)
pureCompareAs :: Comparison -> CompareAs -> Term -> Term -> TCM Bool

Documentation

pureConversion Source #

Arguments

:: TCM b	What to do on `neverUnblock`
-> (Blocker -> TCM b)	What to do on other blockers.
-> (a -> TCM b)	What to do with successful result.
-> TCM a
-> TCM b

runPureConversion :: TCM a -> TCM a Source #

Run conversion without modifying constraint or meta state. A state modification instead throws a pattern violation.

pureEqualTerm :: Type -> Term -> Term -> TCM Bool Source #

Don't catch pattern violation.

pureBlockOrEqualTerm :: Type -> Term -> Term -> TCM (Either Blocker Bool) Source #

Compare terms, catch and return pattern violation.

pureBlockOrEqualTermPureTCM :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool) Source #

pureBlockOrEqualType :: Type -> Type -> TCM (Either Blocker Bool) Source #

pureBlockOrEqualTypePureTCM :: PureTCM m => Type -> Type -> m (Either Blocker Bool) Source #

pureCompareAs :: Comparison -> CompareAs -> Term -> Term -> TCM Bool Source #