Some refactor in Radium crate
This refactor should go through many small steps to make sure that the whole process is merged.
In this branch, multiple attempt and proof-of-concept has been done:
- Use
derive_moreforDisplayfor no-or-few logicfmtfunctions - Use
indocfor bigger blocks - Use
radiumto do the.to_string()logic
In addition, the overall process is to make the radium crate with almost no dependencies to other RefinedRust crates, and to make it as small as possible, since radium should only contain logic for the Coq proof assistant:
- A
RefCell<Option<T>>fromradiumchanged to a simpler type, and the logic is now reflected by aOnceCellintranslation:- Done with
AbstractStructUse:RefCell<Option<AbstractStruct>>toOption<AbstractStruct> - Done with
AbstractEnumUse:RefCell<Option<AbstractEnum>>toAbstractEnum
- Done with
- The dependency of
rrconfiggot removed
Edited by Vincent Lafeychine