Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Tej Chajed
stdpp
Commits
3774c94b
Commit
3774c94b
authored
Aug 17, 2016
by
Ralf Jung
Browse files
Make coqchk slightly happier with prelude/pretty
Unfortunately, it still fails in iris.prelude.pretty.pretty_N_inj
parent
26a59d24
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/pretty.v
View file @
3774c94b
...
...
@@ -32,7 +32,8 @@ Lemma pretty_N_go_step x s :
=
pretty_N_go
(
x
`
div
`
10
)
(
String
(
pretty_N_char
(
x
`
mod
`
10
))
s
).
Proof
.
unfold
pretty_N_go
;
intros
;
destruct
(
wf_guard
32
N
.
lt_wf_0
x
).
unfold
pretty_N_go_help
;
fold
pretty_N_go_help
.
destruct
wf_guard
.
(* this makes coqchk happy. *)
unfold
pretty_N_go_help
at
1
;
fold
pretty_N_go_help
.
by
destruct
(
decide
(
0
<
x
)%
N
)
;
auto
using
pretty_N_go_help_irrel
.
Qed
.
Instance
pretty_N
:
Pretty
N
:
=
λ
x
,
pretty_N_go
x
""
%
string
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment