diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 649fe3eb23..bfb8f9d92b 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -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