-
Notifications
You must be signed in to change notification settings - Fork 108
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
lib: produce _def and _val thms in value_type
Produce a _def theorem for the value type that provides direct symbolic access to the right-hand side of the value_type definition. This avoids having to unfold those terms in subsequent proofs. The numeric value as as term is still available as <type-name>_val. This restricts value_type to nat/int inputs, i.e. word is no longer accepted on the rhs (so far unused). A manual cast to nat on the rhs will still work. Signed-off-by: Gerwin Klein <[email protected]>
- Loading branch information
Showing
2 changed files
with
69 additions
and
24 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters