Agda.TypeChecking.Rewriting.Clause

Converting clauses to rewrite rules

getClausesAsRewriteRules :: (HasConstInfo m, MonadFresh NameId m) => QName -> m [RewriteRule]

Get all the clauses of a definition and convert them to rewrite rules.

clauseQName :: (HasConstInfo m, MonadFresh NameId m) => QName -> Int -> m QName

Generate a sensible name for the given clause

clauseToRewriteRule :: QName -> QName -> Clause -> Maybe RewriteRule

clauseToRewriteRule f q cl converts the clause cl of the function f to a rewrite rule with name q. Returns Nothing if clauseBody cl is Nothing. Precondition: clauseType cl is not Nothing.

class ToNLPat a b where

Minimal complete definition

Nothing

Methods

toNLPat :: a -> b

default toNLPat :: (ToNLPat a' b', Functor f, a ~ f a', b ~ f b') => a -> b

Instances

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Arg DeBruijnPattern -> Elim' NLPat

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat

ToNLPat a b => ToNLPat (Abs a) (Abs b)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Abs a -> Abs b

ToNLPat a b => ToNLPat (Dom a) (Dom b)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b

ToNLPat a b => ToNLPat (Elim' a) (Elim' b)

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Elim' a -> Elim' b

ToNLPat a b => ToNLPat [a] [b]

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: [a] -> [b]