dev experiencegood first issuerefactoring
Repository-Metriken
- Stars
- (1.169 Sterne)
- PR-Merge-Metriken
- (PR-Metriken ausstehend)
Beschreibung
Cakeml currently uses num option in various places where an extended numeral is more appropriate.
for example in wordlang stack_size is a num option where NONE means the stack is unbounded.
This result in slightly unintuitive defintions written in ways like
OPTION_MAP2 $+ a b
option_le defined with option_le SOME _ NONE.
Proof are also harder where many just end up case splitting on the option.
On brief search in the HOL repo there appears to be
xnum developed in examples/HolCheck/ctlScript.sml.
That should probably be refactored out into a separate file + more syntax sugar to allow stuff like 0e to be a 0 : xnum