Agda-2.2.10: A dependently typed functional programming language and proof assistant




flexiblePatterns :: [NamedArg Pattern] -> FlexibleVarsSource

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]Source

Compute the dot pattern instantiations.

isSolvedProblem :: Problem -> BoolSource

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



:: 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 ConstraintsSource

Check that a dot pattern matches it's instantiation.

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

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 aSource

Bind as patterns

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

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



:: Clause

The entire clause.

-> [NamedArg Pattern]

The patterns.

-> Type

The expected type.

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


-> TCM a 

Check a LHS. Main function.