Agda.TypeChecking.Patterns.Internal

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

Documentation

class TermToPattern a b where

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

Minimal complete definition

Nothing

Methods

termToPattern :: a -> TCM b

default termToPattern :: (TermToPattern a' b', Traversable f, a ~ f a', b ~ f b') => a -> TCM b

Instances

DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a)

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Term -> TCM (Pattern' a)

TermToPattern a b => TermToPattern (Arg a) (Arg b)

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Arg a -> TCM (Arg b)

TermToPattern a b => TermToPattern [a] [b]

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: [a] -> TCM [b]

TermToPattern a b => TermToPattern (Named c a) (Named c b)

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Named c a -> TCM (Named c b)

dotPatternsToPatterns :: forall a. DeBruijn (Pattern' a) => Pattern' a -> TCM (Pattern' a)