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

doc: remove Trepplein example (Lean 3) (#7197)

Browse source 
This PR removes a reference to Trepplein (Lean 3) in the documentation.

Co-authored-by: euprunin <euprunin@users.noreply.github.com>
This commit is contained in:
euprunin 2025-02-23 22:39:45 +01:00 • committed by GitHub
parent ad1e04c826
commit c3b01fbd53
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Core.lean
View file

@ -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.
-/