| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Rules.LHS

Synopsis

data DotPatternInst = DPI Expr Term Type
data AsBinding = AsB Name Term Type
flexiblePatterns :: [NamedArg Pattern] -> FlexibleVars
dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Type] -> [DotPatternInst]
instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]
isSolvedProblem :: Problem -> Bool
noShadowingOfConstructors :: Clause -> Problem -> TCM ()
checkDotPattern :: DotPatternInst -> TCM Constraints
bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
checkLeftHandSide :: Clause -> [NamedArg Pattern] -> Type -> (Telescope -> Telescope -> [Term] -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a) -> TCM a
noPatternMatchingOnCodata :: MonadTCM tcm => [(Bool, Arg Pattern)] -> tcm ()

Documentation

data DotPatternInst | Source

Constructors

DPI Expr Term Type |

Instances

Subst DotPatternInst
PrettyTCM DotPatternInst

data AsBinding | Source

Constructors

AsB Name Term Type |

Instances

Raise AsBinding
Subst AsBinding
PrettyTCM AsBinding

flexiblePatterns :: [NamedArg Pattern] -> FlexibleVars | Source

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.

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

isSolvedProblem :: Problem -> Bool | Source

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

noShadowingOfConstructors | Source

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

Check that a dot pattern matches it's instantiation.

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

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

Bind as patterns

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

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

checkLeftHandSide | Source

:: |
=> 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 | Source

:: MonadTCM tcm |
=> [(Bool, Arg Pattern)] | True stands for dependent pattern matching.
-> tcm () |

Produced by Haddock version 2.4.2