| Safe Haskell | Safe-Inferred |
|---|---|
| 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 :: forall a. 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 :: (TermToPattern a' b', Traversable f, a ~ f a', b ~ f b') => a -> TCM b Source #
Instances
| DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # | |
Defined in Agda.TypeChecking.Patterns.Internal | |
| TermToPattern a b => TermToPattern (Arg a) (Arg b) Source # | |
Defined in Agda.TypeChecking.Patterns.Internal | |
| TermToPattern a b => TermToPattern [a] [b] Source # | |
Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: [a] -> TCM [b] Source # | |
| TermToPattern a b => TermToPattern (Named c a) (Named c b) Source # | |
Defined in Agda.TypeChecking.Patterns.Internal | |