Ethos 0.1.1

This release of Ethos is associated with the 1.2.1 release of the SMT solver cvc5.

• When parsing Eunoia signatures, decimals and hexidecimals are never normalized, variables in binders are always unique for their name and type, and let is never treated as a builtin way of specifying macros. The options --no-normalize-dec, --no-normalize-hex, --binder-fresh, and --no-parse-let now only apply when parsing proofs and reference files.
• Adds a new option --normalize-num, which also only applies when reference parsing. This option treats numerals as rationals, which can be used when parsing SMT-LIB inputs in logics where numerals are shorthand for rationals.
• Makes the set-option command available in proofs and Eunoia files.
• Adds --include=X and --reference=X to the command line interface for including (reference) files.
• Fixed the disambiguation of overloaded symbols that are not applied to arguments.
• Fixed the interpretation of operators that combine opaque and ordinary arguments.
• Fixed a bug in the evaluation of eo::cons for left associative operators, which would construct erroneous terms.
• Adds support for eo::dt_constructors which returns the list of constructors associated with a datatype, and eo::dt_selectors which returns the list of selectors associated with a datatype constructor. These operators make use of a type eo::List, which is now part of the background signature assumed by Ethos.
• Fixed parser for the singleton case of declare-datatype.