ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Rewriting.Clause

1 class
3 values

PackageAgda-2.8.0.2
Exports4
LanguageHaskell2010
LicenceMIT
SourceClause.hs

Converting clauses to rewrite rules

4 declarations

valuegetClausesAsRewriteRules

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

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

valueclauseQName

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

Generate a sensible name for the given clause

valueclauseToRewriteRule

:: (MonadTCEnv m, ReadTCState m)
=> QName
-> QName
-> Clause
-> m (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.

classclass ToNLPat a b where

Methods

toNLPat :: a -> b

Instances6ToNLPat

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
ToNLPat a b => ToNLPat (Abs a) (Abs b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
ToNLPat a b => ToNLPat (Dom a) (Dom b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
ToNLPat a b => ToNLPat (Elim' a) (Elim' b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
ToNLPat a b => ToNLPat [a] [b]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause