From baae065f3c13bd9691e664df8490c7bd82b08a49 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Thu, 10 Sep 2026 17:35:39 -0500 Subject: [PATCH 1/2] chore(PFunctor): drop simp tags from non-universe generic lemmas --- Cslib/Foundations/Data/PFunctor/Free.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index a29e974704..7b391f4cb4 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -87,7 +87,6 @@ variable {P : PFunctor.{uA, uB}} {α β γ : Type*} instance : Pure (P.FreeM) where pure := .pure -@[simp] theorem pure_eq_pure : (FreeM.pure : α → P.FreeM α) = pure := rfl /-- Lift a shape of the base polynomial functor into the free monad. -/ @@ -108,8 +107,7 @@ protected def bind : P.FreeM α → (α → P.FreeM β) → P.FreeM β instance : Bind (P.FreeM) where bind := .bind -/-- Note that this lemma does not always apply, as it is universe-constrained by `Bind.bind`. -/ -@[simp] +/-- Not marked `simp` since it is not universe level generic -/ theorem bind_eq_bind {α β : Type v} : (FreeM.bind : P.FreeM α → _ → P.FreeM β) = Bind.bind := rfl From 11abbb5f74dd77813c826302e60645adacb48ff1 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Thu, 10 Sep 2026 17:42:49 -0500 Subject: [PATCH 2/2] missing period --- Cslib/Foundations/Data/PFunctor/Free.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index 7b391f4cb4..3123c66eef 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -107,7 +107,7 @@ protected def bind : P.FreeM α → (α → P.FreeM β) → P.FreeM β instance : Bind (P.FreeM) where bind := .bind -/-- Not marked `simp` since it is not universe level generic -/ +/-- Not marked `simp` since it is not universe level generic. -/ theorem bind_eq_bind {α β : Type v} : (FreeM.bind : P.FreeM α → _ → P.FreeM β) = Bind.bind := rfl