pub fn derive_dec_eq(ctx: &Context, ind: &str) -> KernelResult<(Term, Term)>Expand description
decEqI : Π(A…). Π(dA_i : Π(u v : A_i). Decidable (Eq A_i u v))…. Π(a b : I A…). Decidable (Eq (I A…) a b)
Lean’s deriving DecidableEq, as a term. Structural recursion on a, then a case on b:
DIFFERENT constructors are refuted by derive_no_confusion at P := False; the SAME
constructor decides its fields left to right, assembling the positive proof by iterated
transport (one Eq_rec_dep per field, rewriting one argument of the constructor at a time)
and the negative one from field-k injectivity, again via noConfusion.
A parametric inductive gets one decidable-equality PREMISE per type parameter, exactly as
Lean’s instDecidableEqList [DecidableEq α] does.
A field’s own decision procedure is resolved as: the inductive itself (the recursion), a
type parameter (its premise), or a monomorphic T with decEqT already in scope (the
prelude’s decEqNat/decEqBool, or an earlier derivation). Anything else is REFUSED with
the field named — a decision procedure we cannot actually exhibit must not be claimed.