Skip to content
Snippets Groups Projects
Commit 9fefd07d authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent cd778dae
No related branches found
No related tags found
No related merge requests found
...@@ -22,7 +22,7 @@ Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string := ...@@ -22,7 +22,7 @@ Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string :=
(String (pretty_N_char (x `mod` 10)) s) (String (pretty_N_char (x `mod` 10)) s)
| right _ => s | right _ => s
end. end.
(* The argument [S (N.size_nat x)] of [wf_guard] makes sure that computation (** The argument [S (N.size_nat x)] of [wf_guard] makes sure that computation
works if [x] is a closed term, but that it blocks if [x] is an open term. The works if [x] is a closed term, but that it blocks if [x] is an open term. The
latter prevents unexpected stack overflows, see [tests/pretty.v]. *) latter prevents unexpected stack overflows, see [tests/pretty.v]. *)
Definition pretty_N_go (x : N) : string string := Definition pretty_N_go (x : N) : string string :=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment