theorem RelationNamedState.mk.sizeOf_spec

theorem RelationNamedState.mk.sizeOf_spec
theorem RelationNamedState.mk.sizeOf_spec
: ∀ (params iparams : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (args : Array (Lean.TSyntax `ident))
  (conjuncts : Array (Lean.Name × Lean.TSyntax `term)) (nextInst : Nat),
  sizeOf (a52pkb71.RelationNamedState.mk params iparams args conjuncts nextInst) =
    1 + sizeOf params + sizeOf iparams + sizeOf args + sizeOf conjuncts + sizeOf nextInst

Published by @sam · Jul 17, 2026

View source in a52pkb71

Definitional, with no premises to accept.