HoareSyntax

📁 Source: MRiscX/Parser/HoareSyntax.lean

Statistics

Metric	Count
Definitions hoare_assignment, hoare_assignment_chain, hoare_assignment_term, hoare_term, quot, quot, hoare_assignment_chain_, quot, quot, «hoare_assignmentMem[_]<-_», «hoare_assignmentMem[_]←_», «hoare_assignmentPc++», «hoare_assignmentPc←_», «hoare_assignmentX[_]<-_», «hoare_assignmentX[_]←_», «hoare_assignment_chain_;__1», «hoare_assignment_chain_;__2», «hoare_assignment_chain_;_», «hoare_assignment_term⟦_⟧», «hoare_assignment_term⟦⟧», «hoare_term___⦃_⦄_↦⟨_|_⟩⦃_⦄_1», «hoare_term___⦃_⦄_↦⟨_|_⟩⦃_⦄», «termLabels[_]», «termMem[_]», «termX[_]», «term⦃_⦄», «term⸨pc⸩», «term⸨terminated⸩»	28
Theorems	0
Total	28

Lean.Parser.Category

Definitions

Name	Category	Theorems
hoare_assignment 📖	CompOp	—
hoare_assignment_chain 📖	CompOp	—
hoare_assignment_term 📖	CompOp	—
hoare_term 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
hoare_assignment_chain_ 📖	CompOp	—
«hoare_assignmentMem[_]<-_» 📖	CompOp	—
«hoare_assignmentMem[_]←_» 📖	CompOp	—
«hoare_assignmentPc++» 📖	CompOp	—
«hoare_assignmentPc←_» 📖	CompOp	—
«hoare_assignmentX[_]<-_» 📖	CompOp	—
«hoare_assignmentX[_]←_» 📖	CompOp	—
«hoare_assignment_chain_;__1» 📖	CompOp	—
«hoare_assignment_chain_;__2» 📖	CompOp	—
«hoare_assignment_chain_;_» 📖	CompOp	—
«hoare_assignment_term⟦_⟧» 📖	CompOp	—
«hoare_assignment_term⟦⟧» 📖	CompOp	—
«hoare_term___⦃_⦄_↦⟨_|_⟩⦃_⦄_1» 📖	CompOp	—
«hoare_term___⦃_⦄_↦⟨_|_⟩⦃_⦄» 📖	CompOp	—
«termLabels[_]» 📖	CompOp	—
«termMem[_]» 📖	CompOp	—
«termX[_]» 📖	CompOp	—
«term⦃_⦄» 📖	CompOp	—
«term⸨pc⸩» 📖	CompOp	—
«term⸨terminated⸩» 📖	CompOp	—

hoare_assignment

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

hoare_assignment_chain

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

hoare_assignment_term

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

hoare_term

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

---

← Back to Index