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 (c424c6bg.RelationNamedState.mk params iparams args conjuncts nextInst) =
    1 + sizeOf params + sizeOf iparams + sizeOf args + sizeOf conjuncts + sizeOf nextInst

Published by @sam · Jul 4, 2026

View source in c424c6bg

Definitional, with no premises to accept.