Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Rewriting.Clause

Contents

Converting clauses to rewrite rules

Synopsis

getClausesAsRewriteRules :: (HasConstInfo m, MonadFresh NameId m) => QName -> m [RewriteRule]
clauseQName :: (HasConstInfo m, MonadFresh NameId m) => QName -> Int -> m QName
clauseToRewriteRule :: QName -> QName -> Clause -> Maybe RewriteRule
class ToNLPat a b where
- toNLPat :: a -> b

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 :: (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 Methods toNLPat :: Arg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
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 #