clean up

lecopivo · Jul 27, 2023 · ba1a6bb · ba1a6bb
1 parent 4534a91
commit ba1a6bb
Showing 1 changed file with 0 additions and 7 deletions.
diff --git a/SciLean/FunctionSpaces/Continuous/Basic.lean b/SciLean/FunctionSpaces/Continuous/Basic.lean
@@ -119,13 +119,6 @@ def Continuous.fpropExt : FPropExt where
     mkAppM ``Continuous.comp_rule #[g,hg,f,hf]
 
   lambdaLetRule _ f g := do
-    -- let thm : SimpTheorem :=
-    -- {
-    --   proof  := mkConst ``Continuous.let_rule 
-    --   origin := .decl ``Continuous.let_rule 
-    --   rfl    := false
-    -- }
-    -- FProp.tryTheorem? e thm (fun _ => pure none)
 
     let HF ← mkAppM ``Continuous #[(← mkUncurryFun 2 f)]
     let .some hf ← FProp.fprop HF