- simple: Lake.Name → List Lake.Name → Lean.OpenDecl
- explicit: Lake.Name → Lake.Name → Lean.OpenDecl
Data for representing open
commands
Instances For
Equations
- Lean.instBEqOpenDecl = { beq := Lean.beqOpenDecl✝ }
Equations
- Lean.OpenDecl.instInhabitedOpenDecl = { default := Lean.OpenDecl.simple Lean.Name.anonymous [] }
Equations
- One or more equations did not get rendered due to their size.