Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rewriting.Clause

Synopsis

Converting clauses to rewrite rules

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

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

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

Generate a sensible name for the given clause

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

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 Source #

Minimal complete definition

Nothing

Methods

toNLPat :: a -> b Source #

default toNLPat :: forall a' b' (f :: Type -> Type). (ToNLPat a' b', Functor f, a ~ f a', b ~ f b') => a -> b Source #

Instances

Instances details
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat a b => ToNLPat (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Abs a -> Abs b Source #

ToNLPat a b => ToNLPat (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b Source #

ToNLPat a b => ToNLPat (Elim' a) (Elim' b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Elim' a -> Elim' b Source #

ToNLPat a b => ToNLPat [a] [b] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: [a] -> [b] Source #