Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Patterns.Internal

Description

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

Synopsis

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

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 #