Given a metavariable mvarId
representing the goal
Ctx |- T
and an expression e : I A j
, where I A j
is an inductive datatype where A
are parameters,
and j
the indices. Generate the goal
Ctx, j' : J, h' : I A j' |- j == j' -> e == h' -> T
Remark: (j == j' -> e == h')
is a "telescopic" equality.
Remark: j
is sequence of terms, and j'
a sequence of free variables.
The result contains the fields
mvarId
: the new goalindicesFVarIds
:j'
idsfvarId
:h'
idnumEqs
: number of equations in the target
If varName?
is not none, it is used to name h'
.
Equations
Instances For
Similar to generalizeTargets
but customized for the casesOn
motive.
Given a metavariable mvarId
representing the
Ctx, h : I A j, D |- T
where fvarId
is h
s id, and the type I A j
is an inductive datatype where A
are parameters,
and j
the indices. Generate the goal
Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T
Remark: (j == j' -> h == h')
is a "telescopic" equality.
Remark: j
is sequence of terms, and j'
a sequence of free variables.
The result contains the fields
mvarId
: the new goalindicesFVarIds
:j'
idsfvarId
:h'
idnumEqs
: number of equations in the target
Equations
Instances For
- inductiveVal : InductiveVal
- casesOnVal : DefinitionVal
- nminors : Nat
- majorDecl : LocalDecl
- majorTypeFn : Expr
Instances For
Equations
Instances For
Apply casesOn
using the free variable majorFVarId
as the major premise (aka discriminant).
givenNames
contains user-facing names for each alternative.
useNatCasesAuxOn
is a temporary hack for thercases
family of tactics. Do not use it, as it is subject to removal. It enables usingNat.casesAuxOn
instead ofNat.casesOn
, which causes case splits onn : Nat
to be represented as0
andn' + 1
rather than asNat.zero
andNat.succ n'
.
Equations
Instances For
Split the goal in two subgoals: one containing the hypothesis h : p
and another containing h : ¬ p
.
Equations
Instances For
Given dec : Decidable p
, split the goal in two subgoals: one containing the hypothesis h : p
and another containing h : ¬ p
.