Agda.TypeChecking.Patterns.Internal

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

Synopsis

classclass TermToPattern a b where

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

Instances4TermToPattern

DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Internal
TermToPattern a b => TermToPattern (Arg a) (Arg b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Internal
TermToPattern a b => TermToPattern [a] [b]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Internal
TermToPattern a b => TermToPattern (Named c a) (Named c b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Internal

valuedotPatternsToPatterns