| 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
- dotPatternsToPatterns :: forall a. DeBruijn (Pattern' a) => Pattern' a -> TCM (Pattern' a)
Documentation
class TermToPattern a b where #
Convert a term (from a dot pattern) to a DeBruijn pattern.
Methods
termToPattern :: a -> TCM b #
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 [a] [b] # | |
Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: [a] -> TCM [b] # | |
| 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 (Named c a) (Named c b) # | |
Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Named c a -> TCM (Named c b) # | |