max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: mark Nat.decEq as [reducible]

Browse source 
It is used by the `noConfusionType` construction for enumeration types,
and we want it to reduce even when the reducibility setting is
`TransparencyMode.reducible` as for other inductive types.

see issue #1016
This commit is contained in:
Leonardo de Moura 2022-02-14 12:00:29 -08:00
parent 93d5351fba
commit ee9fcd30e8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Prelude.lean
View file

@ -616,7 +616,7 @@ theorem Nat.ne_of_beq_eq_false : {n m : Nat} → Eq (beq n m) false → Not (Eq
have : Eq (beq n m) false := h₁
Nat.noConfusion h₂ (fun h₂ => absurd h₂ (ne_of_beq_eq_false this))
@[extern "lean_nat_dec_eq"]
@[reducible, extern "lean_nat_dec_eq"]
protected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) :=
match h:beq n m with
| true => isTrue (eq_of_beq_eq_true h)