Expand description
This Module is responsible for converting the .llbc files to .v files. There is the potential for it to be extended to convert to other formats also supported by AENEAS. I will need to experiment with verification to see what is most useful
Functions§
- coq_
conversion - ============================================================================ —————————–– CoQ Conversion —————————–