Agda.TypeChecking.Rewriting

Documentation

verifyBuiltinRewrite :: Term -> Type -> TCM ()

data RelView

Constructors

RelView

Fields

relViewTel :: Telescope

relViewDelta :: ListTel

relViewType :: Type

t.

relViewType' :: Type

t'.

relViewCore :: Type

core.

relView :: Type -> TCM (Maybe RelView)

addRewriteRule :: QName -> TCM ()

addRewriteRules :: QName -> RewriteRules -> TCM ()

Append rewrite rules to a definition.

updateRewriteRules :: (RewriteRules -> RewriteRules) -> Definition -> Definition

Lens for RewriteRules.

rewriteWith :: Maybe Type -> Term -> RewriteRule -> TCM (Maybe Term)

rewriteWith t v rew tries to rewrite v : t with rew, returning the reduct if successful.

rewrite :: Term -> TCM (Maybe Term)

rewrite t tries to rewrite a reduced term.