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

Safe HaskellNone

Agda.TypeChecking.Rules.LHS.Split

Synopsis

Documentation

asView :: Pattern -> ([Name], Pattern)Source

TODO: move to Agda.Syntax.Abstract.View

expandLitPattern :: NamedArg Pattern -> TCM (NamedArg Pattern)Source

TODO: move somewhere else

splitProblem :: Problem -> TCM (Either SplitError SplitProblem)Source

Split a problem at the first constructor of datatype type. Implicit patterns should have been inserted.

wellFormedIndices :: Type -> TCM ()Source

Takes a type, which must be a data or record type application, and checks that the indices are constructors (or literals) applied to distinct variables which do not occur free in the parameters. For the purposes of this check parameters count as constructor arguments; parameters are reconstructed from the given type.

Precondition: The type must be a data or record type application.

withTypesFrom :: Args -> Type -> TCM [(Arg Term, Dom Type)]Source

args `withTypesFrom` t returns the arguments args paired up with their types, taken from t, which is assumed to be a length args-ary pi.

Precondition: t has to start with length args pis.