 Ariadne Devos
|
a93c558d1c
Generalise sHT_X_to_u32's overflow criterium to other bases
|
4 years ago |
|
Ariadne Devos
|
df2fb42ed1
State positivity of signless positional representations
|
4 years ago |
|
Ariadne Devos
|
dc530728da
Correct license of <lex/nat-uphex.c>
|
4 years ago |
|
Ariadne Devos
|
d7af289127
Add missing mathematical definitions
|
4 years ago |
|
Ariadne Devos
|
cad4f3bcc6
Abstract sHT_uphex_to_u32 over bases
|
4 years ago |
|
Ariadne Devos
|
632f8e0ad7
Implement sHT_uphex_to_u32
|
4 years ago |
|
Ariadne Devos
|
283180194c
Specify upper-case hexadecimal number lexing
|
4 years ago |
|
Ariadne Devos
|
26dbe4c159
Specify non-overflowing multiply-add
|
4 years ago |
|
Ariadne Devos
|
c87a34ad2c
State bounds on decimal_num_val etc.
|
4 years ago |
|
Ariadne Devos
|
122268f584
Precompute powers of 16 in lemma for overflow checking
|
4 years ago |
|
Ariadne Devos
|
626ccba31b
State induction lemma's for decimal_num_val etc.
|
4 years ago |
|
Ariadne Devos
|
912ccb9227
Apply 'static' attribute to tiny, inline functions
|
4 years ago |
|
Ariadne Devos
|
c45315ee1f
Drop superfluous, overly strict precondition of sHT_index_nospec
|
4 years ago |
|
Ariadne Devos
|
0da2a695a6
Give upper bounds for decimal_val_plural etc.
|
4 years ago |
|
Ariadne Devos
|
4e1e5f0901
State, not prove, vector_lt induction lemmas
|
4 years ago |
|
Ariadne Devos
|
de68d31912
Assert induction lemmas for decimal_val_plural etc.
|
4 years ago |
|
Ariadne Devos
|
3af0e47d99
Formalise speculative conditions in <sHT/lex/digit.h>
|
4 years ago |
|
Ariadne Devos
|
b2ceeb7a0d
Add missing include
|
4 years ago |
|
Ariadne Devos
|
886ba1f711
Correct <sHT/test.h> specifications
|
4 years ago |
|
Ariadne Devos
|
56d1a54c6d
Update <sHT/test.h> note to current knowledge and goals
|
4 years ago |
|
Ariadne Devos
|
29e1e18973
Model speculation
|
4 years ago |
|
Ariadne Devos
|
97746de5a1
Lift C arrays to vectors / lists
|
4 years ago |
|
Ariadne Devos
|
c721066d6e
Define decimal hexadecimal numbers
|
4 years ago |
|
Ariadne Devos
|
49d85172b7
Map hex_val etc. over vectors
|
4 years ago |
|
Ariadne Devos
|
76eeb76aac
Specify Kleene closure of digits
|
4 years ago |
|
Ariadne Devos
|
7165e7d088
Allow hex_val for consistency
|
4 years ago |
|
Ariadne Devos
|
91c13fdcbf
Specify helper construction for digits lexing
|
4 years ago |
|
Ariadne Devos
|
6288f3e145
Specify exponentiation in ℤ
|
4 years ago |
|
Ariadne Devos
|
94b7649f20
Approximate the sign of ∏v
|
4 years ago |
|
Ariadne Devos
|
d3803dfc77
Delete dubious, unproved lemma
|
4 years ago |
