Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rewriting.Clause

Contents

- Converting clauses to rewrite rules

Synopsis

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

# Converting clauses to rewrite rules

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