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:
derive_more
for Display
for no-or-few logic fmt
functionsindoc
for bigger blocksradium
to do the .to_string()
logicIn 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:
RefCell<Option<T>>
from radium
changed to a simpler type, and the logic is now reflected by a OnceCell
in translation
:
AbstractStructUse
: RefCell<Option<AbstractStruct>>
to Option<AbstractStruct>
AbstractEnumUse
: RefCell<Option<AbstractEnum>>
to AbstractEnum
rrconfig
got removed