From 413a0faf99eebe8a965c70724a4bc6ee09c431df Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 May 2016 17:24:47 -0700 Subject: [PATCH] chore(library/data/nat/bquant): make sure we can generate code for bsub_succ --- library/data/nat/bquant.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index de01aca413..864ba887c1 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -42,11 +42,7 @@ namespace nat λ H, absurd (bex_of_bsub H) (not_bex_zero P) definition bsub_succ {P : nat → Prop} {n : nat} (H : bsub n P) : bsub (succ n) P := - sorry - /- - obtain (w : nat) (Hw : w < n ∧ P w), from H, - and.rec_on Hw (λ hlt hp, tag w (and.intro (lt.step hlt) hp)) - -/ + subtype.rec_on H (λ w Hw, tag w (and.rec_on Hw (λ hlt hp, and.intro (lt.step hlt) hp))) theorem bex_succ {P : nat → Prop} {n : nat} (H : bex n P) : bex (succ n) P := sorry