| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rewriting.Clause
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
Instances
| ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # | |
Defined in Agda.TypeChecking.Rewriting.Clause | |
| ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |
Defined in Agda.TypeChecking.Rewriting.Clause | |
| ToNLPat a b => ToNLPat (Abs a) (Abs b) Source # | |
| ToNLPat a b => ToNLPat (Dom a) (Dom b) Source # | |
| ToNLPat a b => ToNLPat (Elim' a) (Elim' b) Source # | |
| ToNLPat a b => ToNLPat [a] [b] Source # | |
Defined in Agda.TypeChecking.Rewriting.Clause | |