feat: ext lemma for Thunk (#842)

leanprover-community · Jun 14, 2024 · 15d42e1 · 15d42e1
1 parent 0f5b287
commit 15d42e1
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/Batteries.lean b/Batteries.lean
@@ -35,6 +35,7 @@ import Batteries.Data.Range
 import Batteries.Data.Rat
 import Batteries.Data.String
 import Batteries.Data.Sum
+import Batteries.Data.Thunk
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
 import Batteries.Lean.AttributeExtra

diff --git a/Batteries/Data/Thunk.lean b/Batteries/Data/Thunk.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE
+Authors: François G. Dorais, et al.
+-/
+
+namespace Thunk
+
+@[ext] protected theorem ext : {a b : Thunk α} → a.get = b.get → a = b
+  | {..}, {..}, heq => congrArg _ <| funext fun _ => heq