The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
Use `byte` based strings for proof mode
Newer versions of Coq have a type byte with 256 constructors. We could use strings based on byte in the proofmode. Maybe that gives a significant speed up compared to the current ascii based strings.
@tchajed said the construction of byte based strings does not exist in the Coq stdlib but can be defined as:
From Coq Require Import Init.Byte.
Record bytes := bytes_from_list { bytes_to_list : list byte }.
Declare Scope bytestring_scope.
Open Scope bytestring_scope.
String Notation bytes bytes_from_list bytes_to_list : bytestring_scope.
Definition foo : bytes := "foo".