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

chore(library/data/nat/bquant): make sure we can generate code for bsub_succ

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-23 17:24:47 -07:00
parent d7e863c3f4
commit 413a0faf99
1 changed files with 1 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/nat/bquant.lean
View file

@ -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