Get all the clauses of a definition and convert them to rewrite rules.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Rewriting.Clause
Synopsis
- value getClausesAsRewriteRules
- value clauseQName
- value clauseToRewriteRule
- class ToNLPat
- PackageAgda-2.8.0.2
- Exports4
- LanguageHaskell2010
- LicenceMIT
- SourceClause.hs
Converting clauses to rewrite rules
Generate a sensible name for the given clause
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.
Methods
toNLPat :: a -> b
Instances6ToNLPat
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ClauseToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ClauseToNLPat a b => ToNLPat (Abs a) (Abs b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ClauseToNLPat a b => ToNLPat (Dom a) (Dom b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ClauseToNLPat a b => ToNLPat (Elim' a) (Elim' b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ClauseToNLPat a b => ToNLPat [a] [b]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause