|
|
|
|
|
|
by Rochus
124 days ago
|
|
|
Thanks for the hint. The "LeanMachines" project literally seems to recreate Event-B constructs (contexts, machines, events, and refinement proof obligations) inside the Lean 4 proof assistant (using Lean 4 as a "host language"). |
|
|