max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: missing @[ext] attribute on monad transformer ext lemmas (#6008)

Browse source
This commit is contained in:
Kim Morrison 2024-11-08 17:53:49 +11:00 • committed by GitHub
parent 680177049f
commit 1870c003d0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Control/Lawful/Instances.lean
View file

@ -7,6 +7,7 @@ prelude
import Init.Control.Lawful.Basic
import Init.Control.Except
import Init.Control.StateRef
import Init.Ext
open Function
@ -14,7 +15,7 @@ open Function
namespace ExceptT
theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
@[ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
simp [run] at h
assumption
@ -105,7 +106,7 @@ instance : LawfulFunctor (Except ε) := inferInstance
namespace ReaderT
theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
@[ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
simp [run] at h
exact funext h
@ -167,7 +168,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
namespace StateT
theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
@[ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
funext h
@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=