- fixed : CongrArgKind
It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides.
- fixedNoParam : CongrArgKind
It is not a parameter for the congruence theorem, the theorem was specialized for this parameter. This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it.
- eq : CongrArgKind
The lemma contains three parameters for this kind of argument
a_i
,b_i
andeq_i : a_i = b_i
.a_i
andb_i
represent the left and right hand sides, andeq_i
is a proof for their equality. - cast : CongrArgKind
The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two. They correspond to arguments that are subsingletons/propositions.
- heq : CongrArgKind
The lemma contains three parameters for this kind of argument
a_i
,b_i
andeq_i : HEq a_i b_i
.a_i
andb_i
represent the left and right hand sides, andeq_i
is a proof for their heterogeneous equality. - subsingletonInst : CongrArgKind
For congr-simp theorems only. Indicates a decidable instance argument. The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...]
Instances For
- type : Expr
- proof : Expr
- argKinds : Array CongrArgKind
Instances For
Equations
Instances For
Variant of getCongrSimpKinds
for rewriting just argument 0.
If it is possible to rewrite, the 0th CongrArgKind
is CongrArgKind.eq
,
and otherwise it is CongrArgKind.fixed
. This is used for the arg
conv tactic.
Equations
Instances For
Create a congruence theorem that is useful for the simplifier and congr
tactic.
Equations
Instances For
Create a congruence theorem that is useful for the simplifier.
In this kind of theorem, if the i-th argument is a cast
argument, then the theorem
contains an input a_i
representing the i-th argument in the left-hand-side, and
it appears with a cast (e.g., Eq.drec ... a_i ...
) in the right-hand-side.
The idea is that the right-hand-side of this theorem "tells" the simplifier
how the resulting term looks like.
Equations
Instances For
Equations
Instances For
Create a congruence theorem for f
. The theorem is used in the simplifier.
If subsingletonInstImplicitRhs = true
, the rhs
corresponding to [Decidable p]
parameters
is marked as instance implicit. It forces the simplifier to compute the new instance when applying
the congruence theorem.
For the congr
tactic we set it to false
.
Equations
Instances For
Returns true
if s
is of the form hcongr_<idx>
Equations
Instances For
Similar to mkHCongrWithArity
, but uses reserved names to ensure we don't keep creating the
same congruence theorem over and over again.
Equations
Instances For
Similar to mkCongrSimp?
, but uses reserved names to ensure we don't keep creating the
same congruence theorem over and over again.