-
Etienne Kneuss authored
- Ensurings/Require are now proper purescala trees - Introduce Assert as a tree - Simplify tactics to support arbitrary asserts/errors/inner ensurings - New phase to inject assertions for unsafe calls (array/map access) - Refactor Default and Induction tactic
Etienne Kneuss authored- Ensurings/Require are now proper purescala trees - Introduce Assert as a tree - Simplify tactics to support arbitrary asserts/errors/inner ensurings - New phase to inject assertions for unsafe calls (array/map access) - Refactor Default and Induction tactic
FunctionTemplate.scala 11.46 KiB