From 5345db88774ea295221d26060e1ab2758b5e6a5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Thu, 5 Feb 2026 14:42:36 +0000 Subject: [PATCH] feat: make `Theorem` an `Inhabited` instance (#12324) This PR adds a default `Inhabited` instance to `Theorem` type. The need to do so came up in #12296 , as `Theorem` is one of the entries of the structure which is the key entry of `SimpleScopedEnvExtension`. --- src/Lean/Meta/Sym/Simp/Theorems.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Meta/Sym/Simp/Theorems.lean b/src/Lean/Meta/Sym/Simp/Theorems.lean index b57430f952..5207558b76 100644 --- a/src/Lean/Meta/Sym/Simp/Theorems.lean +++ b/src/Lean/Meta/Sym/Simp/Theorems.lean @@ -24,6 +24,7 @@ structure Theorem where pattern : Pattern /-- Right-hand side of the equation. -/ rhs : Expr + deriving Inhabited instance : BEq Theorem where beq thm₁ thm₂ := thm₁.expr == thm₂.expr