Agda.TypeChecking.Rules.LHS

Documentation

data DotPatternInst

Constructors

DPI Expr Term Type

Instances

Subst DotPatternInst

PrettyTCM DotPatternInst

data AsBinding

Constructors

AsB Name Term Type

Instances

Raise AsBinding

Subst AsBinding

PrettyTCM AsBinding

flexiblePatterns :: [NamedArg Pattern] -> FlexibleVars

Compute the set of flexible patterns in a list of patterns. The result is the deBruijn indices of the flexible patterns. A pattern is flexible if it is dotted or implicit.

dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Type] -> [DotPatternInst]

Compute the dot pattern instantiations.

instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]

isSolvedProblem :: Problem -> Bool

Check if a problem is solved. That is, if the patterns are all variables.

noShadowingOfConstructors

Arguments

:: Clause

The entire clause (used for error reporting).

-> Problem

-> TCM ()

For each user-defined pattern variable in the Problem, check that the corresponding data type (if any) does not contain a constructor of the same name (which is not in scope); this "shadowing" could indicate an error, and is not allowed.

Precondition: The problem has to be solved.

checkDotPattern :: DotPatternInst -> TCM Constraints

Check that a dot pattern matches it's instantiation.

bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a

Bind the variables in a left hand side. Precondition: the patterns should all be VarP, WildP, or ImplicitP and the telescope should have the same size as the pattern list.

bindAsPatterns :: [AsBinding] -> TCM a -> TCM a

Bind as patterns

useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope

Rename the variables in a telescope using the names from a given pattern

checkLeftHandSide

Arguments

:: Clause

The entire clause.

-> [NamedArg Pattern]

The patterns.

-> Type

The expected type.

-> (Telescope -> Telescope -> [Term] -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a)

Continuation.

-> TCM a

Check a LHS. Main function.

noPatternMatchingOnCodata

Arguments

:: MonadTCM tcm

=> [(Bool, Arg Pattern)]

True stands for dependent pattern matching.

-> tcm ()