Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Rules.LHS
Synopsis
- checkLeftHandSide :: forall a. Call -> Maybe QName -> [NamedArg Pattern] -> Type -> Maybe Substitution -> [ProblemEq] -> (LHSResult -> TCM a) -> TCM a
- data LHSResult = LHSResult {
- lhsParameters :: Nat
- lhsVarTele :: Telescope
- lhsPatterns :: [NamedArg DeBruijnPattern]
- lhsHasAbsurd :: Bool
- lhsBodyType :: Arg Type
- lhsPatSubst :: Substitution
- lhsAsBindings :: [AsBinding]
- lhsPartialSplit :: [Int]
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- class IsFlexiblePattern a where
- maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind
- isFlexiblePattern :: a -> TCM Bool
- checkSortOfSplitVar :: (MonadTCM tcm, MonadReduce tcm, MonadError TCErr tcm, LensSort a) => DataOrRecord -> a -> Maybe (Arg Type) -> tcm ()
Documentation
Arguments
:: Call | Trace, e.g. |
-> Maybe QName | The name of the definition we are checking. |
-> [NamedArg Pattern] | The patterns. |
-> Type | The expected type |
-> Maybe Substitution | Module parameter substitution from with-abstraction. |
-> [ProblemEq] | Patterns that have been stripped away by with-desugaring. ^ These should not contain any proper matches. |
-> (LHSResult -> TCM a) | Continuation. |
-> TCM a |
Check a LHS. Main function.
checkLeftHandSide a ps a ret
checks that user patterns ps
eliminate
the type a
of the defined function, and calls continuation ret
if successful.
Result of checking the LHS of a clause.
Constructors
LHSResult | |
Fields
|
Instances
InstantiateFull LHSResult Source # | |
Defined in Agda.TypeChecking.Rules.LHS |
class IsFlexiblePattern a where Source #
A pattern is flexible if it is dotted or implicit, or a record pattern with only flexible subpatterns.
Minimal complete definition
Methods
maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind Source #
isFlexiblePattern :: a -> TCM Bool Source #
Instances
checkSortOfSplitVar :: (MonadTCM tcm, MonadReduce tcm, MonadError TCErr tcm, LensSort a) => DataOrRecord -> a -> Maybe (Arg Type) -> tcm () Source #