Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




flexiblePatterns :: [NamedArg Pattern] -> TCM 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 -> [Dom Type] -> TCM [DotPatternInst]Source

Compute the dot pattern instantiations.

isSolvedProblem :: Problem -> BoolSource

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



:: (Maybe r -> Call)

Trace, e.g., CheckPatternShadowing clause

-> 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 ()Source

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. There could also be ConPs resulting from eta expanded implicit record patterns.

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

Bind as patterns



:: (Maybe r -> Call)

Trace, e.g. CheckPatternShadowing clause

-> [NamedArg Pattern]

The patterns.

-> Type

The expected type a = Γ →.

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


-> TCM a 

Check a LHS. Main function.