Instr

📁 Source: MRiscX/AbstractSyntax/Instr.lean

Statistics

Metric	Count
Definitions Instr, beq, instBEqInstr, beq, instBEqInstr_1, instInhabitedInstr, default, instReprInstr, repr, instToStringInstr	10
Theorems refl	1
Total	11

Instr

Definitions

Name	Category	Theorems
beq 📖	CompOp	1 bridge bridge: refl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl 📖	bridging (complete)	—	beq	beq	beq.eq_1

(root)

Definitions

Name	Category	Theorems
Instr 📖	CompData	2 math math: MState.currInstruction_unfold, MState.runNSteps_currInstruction
instBEqInstr 📖	CompOp	—
instBEqInstr_1 📖	CompOp	—
instInhabitedInstr 📖	CompOp	—
instReprInstr 📖	CompOp	—
instToStringInstr 📖	CompOp	—

instBEqInstr

Definitions

Name	Category	Theorems
beq 📖	CompOp	—

instInhabitedInstr

Definitions

Name	Category	Theorems
default 📖	CompOp	—

instReprInstr

Definitions

Name	Category	Theorems
repr 📖	CompOp	—

---

← Back to Index