HoareElaborator

📁 Source: MRiscX/Elab/HoareElaborator.lean

Statistics

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

(root)

Definitions

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

processHoareTerm

Definitions

Name	Category	Theorems
go 📖	CompOp	—

---

← Back to Index