HoareElaborator

📁 Source: MRiscX/Elab/HoareElaborator.lean

Statistics

Metric	Count
Definitions elabHoareTerm, mriscxSpecToTerm, mriscxSyntaxToTerm, processHoareTerm, go, term__3, «termHoare__⦃_⦄_↦⟨_|_⟩⦃_⦄End», «term___⦃_⦄_↦⟨_|_⟩⦃_⦄», «term_⦃_⦄_↦⟨_|_⟩⦃_⦄», «term⟦_⟧», «term⟦⟧», «term⦃_⦄_1»	12
Theorems	0
Total	12

(root)

Definitions

Name	Category	Theorems
elabHoareTerm 📖	CompOp	—
mriscxSpecToTerm 📖	CompOp	—
mriscxSyntaxToTerm 📖	CompOp	—
processHoareTerm 📖	CompOp	—
term__3 📖	CompOp	—
«termHoare__⦃_⦄_↦⟨_|_⟩⦃_⦄End» 📖	CompOp	—
«term___⦃_⦄_↦⟨_|_⟩⦃_⦄» 📖	CompOp	—
«term_⦃_⦄_↦⟨_|_⟩⦃_⦄» 📖	CompOp	—
«term⟦_⟧» 📖	CompOp	—
«term⟦⟧» 📖	CompOp	—
«term⦃_⦄_1» 📖	CompOp	—

processHoareTerm

Definitions

Name	Category	Theorems
go 📖	CompOp	—

---

← Back to Index