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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Patterns.Internal

Description

Tools to manipulate patterns in internal syntax in the TCM (type checking monad).

Synopsis

- class TermToPattern a b where
  - termToPattern :: a -> TCM b
- dotPatternsToPatterns :: DeBruijn (Pattern' a) => Pattern' a -> TCM (Pattern' a)

# Documentation

class TermToPattern a b where Source #

Convert a term (from a dot pattern) to a DeBruijn pattern.

Minimal complete definition

Nothing

Methods

termToPattern :: a -> TCM b Source #

default termToPattern :: forall a' b' (f :: Type -> Type). (TermToPattern a' b', Traversable f, a ~ f a', b ~ f b') => a -> TCM b Source #

#### Instances

Instances details

DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Term -> TCM (Pattern' a) Source #
TermToPattern a b => TermToPattern (Arg a) (Arg b) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Arg a -> TCM (Arg b) Source #
TermToPattern a b => TermToPattern [a] [b] Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: [a] -> TCM [b] Source #
TermToPattern a b => TermToPattern (Named c a) (Named c b) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Named c a -> TCM (Named c b) Source #

dotPatternsToPatterns :: DeBruijn (Pattern' a) => Pattern' a -> TCM (Pattern' a) Source #