diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-04 20:19:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-04 20:19:01 +0000 |
| commit | 53f83dbdb371e6efe376e0e7be12f15b2886d707 (patch) | |
| tree | a10af767590ab62281c00783cfc34315cfac4f11 /plugins/extraction | |
| parent | a105bc07a504da50f4563793d31f34fa724b2bcb (diff) | |
Ascii: simplier ascii_of_pos, conversion from/to N, proofs about nat-->ascii-->nat
- ascii_of_pos isn't tail-recursive anymore, but recursivity is at most of depth 8.
- (brutal) proof that N_of_ascii (ascii_of_N n) = n for all n<256, same for nat.
Ideally, we could say someday that N_of_ascii (ascii_of_N n) = n mod 256
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13077 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
0 files changed, 0 insertions, 0 deletions