From c3b01fbd534e4fa4b2549ef33f68ad7fcfa9669c Mon Sep 17 00:00:00 2001 From: euprunin Date: Sun, 23 Feb 2025 22:39:45 +0100 Subject: [PATCH] doc: remove Trepplein example (Lean 3) (#7197) This PR removes a reference to Trepplein (Lean 3) in the documentation. Co-authored-by: euprunin --- src/Init/Core.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index ab2f389078..dc42ae1aba 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -2020,7 +2020,7 @@ free variables. The frontend automatically declares a fresh auxiliary constant ` Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using -external type checkers (e.g., Trepplein) that do not implement this feature. +external type checkers that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers. @@ -2055,7 +2055,7 @@ decidability instance can be evaluated to `true` using the lean compiler / inter Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using -external type checkers (e.g., Trepplein) that do not implement this feature. +external type checkers that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers. -/ @@ -2066,7 +2066,7 @@ The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using -external type checkers (e.g., Trepplein) that do not implement this feature. +external type checkers that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers. -/