diff --git a/library/standard/logic/classes/decidable.lean b/library/standard/logic/classes/decidable.lean index 96f83683f..071734005 100644 --- a/library/standard/logic/classes/decidable.lean +++ b/library/standard/logic/classes/decidable.lean @@ -73,3 +73,5 @@ rec_on Ha (assume Hb : b, inl (assume H, Hb)) (assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb))) (assume Hna : ¬a, inl (assume Ha, absurd_elim b Ha Hna)) + +end \ No newline at end of file