Documentation

LeanPool.MRiscX.Basic

Imports

Init
LeanPool.MRiscX.Delab.DelabCode
LeanPool.MRiscX.Elab.CodeElaborator
LeanPool.MRiscX.Elab.HoareElaborator
LeanPool.MRiscX.Hoare.HoareRules
LeanPool.MRiscX.Semantics.Specification
LeanPool.MRiscX.Tactics.CodeProofTactics
LeanPool.MRiscX.Util.BasicTheorems

Imported by

Basic #

This module provides the top-level entry point gathering the MRiscX modules.