From 1f9ab675145426c2e8dbe79b23a3acc15853bf3e Mon Sep 17 00:00:00 2001 From: lecopivo Date: Mon, 24 Jul 2023 18:41:34 -0400 Subject: [PATCH] typo fix --- SciLean/FunctionSpaces/Continuous/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SciLean/FunctionSpaces/Continuous/Basic.lean b/SciLean/FunctionSpaces/Continuous/Basic.lean index b665f060..1b7469de 100644 --- a/SciLean/FunctionSpaces/Continuous/Basic.lean +++ b/SciLean/FunctionSpaces/Continuous/Basic.lean @@ -60,7 +60,7 @@ end SciLean.Continuous -------------------------------------------------------------------------------- --- Register Diferentiable ------------------------------------------------------ +-- Register Continuous --------------------------------------------------------- -------------------------------------------------------------------------------- open Lean Meta SciLean FProp