From 700c911cf700109edd3ced04ae8f4f9624a1d685 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Aug 2014 17:00:01 -0700 Subject: [PATCH] chore(library/standard/logic/class/decidable): add missing 'end' Signed-off-by: Leonardo de Moura --- library/standard/logic/classes/decidable.lean | 2 ++ 1 file changed, 2 insertions(+) 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