Read-only archive. Publishing has closed. GitHub
theorem RelationSlotSpec.mk.inj
theorem RelationSlotSpec.mk.inj
: ∀ {binderTy rawTy : Lean.TSyntax `term} {constraint? : Option (Lean.TSyntax `ident)}
  {binderTy_1 rawTy_1 : Lean.TSyntax `term} {constraint?_1 : Option (Lean.TSyntax `ident)},
  r59jf3ak.RelationSlotSpec.mk binderTy rawTy constraint? =
      r59jf3ak.RelationSlotSpec.mk binderTy_1 rawTy_1 constraint?_1 →
    binderTy = binderTy_1 ∧ rawTy = rawTy_1 ∧ constraint? = constraint?_1

Published by @sam ·

View source in r59jf3ak

Definitional, with no premises to accept.