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

chore: fix build

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-19 07:43:54 -08:00
parent a5ab59a413
commit 966e1df96d
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/Core.lean
View file

@ -704,7 +704,7 @@ theorem decide_false_eq_false (h : Decidable False) : @decide False h = false :=
/-- Similar to `decide`, but uses an explicit instance -/
@[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
decide p (h := d)
decide (h := d)
theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
decide_eq_true (inst := d) h