Comments (2)
PatrickMassot
commented on August 17, 2024
Unfortunately you managed to find an extremely outdated document. See https://leanprover-community.github.io/ for up to date information about the current version of Lean. This GitHub repository is about the next version of Lean which is not yet ready for users (see the README).
from lean4.
catskillsresearch
commented on August 17, 2024
The newer docs point me to this and it just says sorry all the way through. The extremely outdated doc at least works most of the time
http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=1&level=1
It's OK I'll figure it out but my intuition is to go through this oldest stuff first.
from lean4.
Related Issues (20)
- RFC: make `Lean.Meta.setInlineAttribute` a `CoreM Unit`
- Incorrect metadata on pretty-printed signature of `String.append` HOT 2
- Question: How does the Lean LSP server determine whether a file is open? HOT 1
- PANIC at Lean.Expr.appFn! in Fin.isValue, in the presence of metadata
- PANIC at Lean.MVarId.falseOrByContra Lean.Elab.Tactic.FalseOrByContra:55:22: expected one subgoal
- PANIC at Lean.MVarId.falseOrByContra Lean.Elab.Tactic.FalseOrByContra:58:44: expected one sugoal [sic]
- RFC: Exclude `.lake` directory from backups with `CACHEDIR.TAG`
- Lemmas about `private` defs are not `private` by default HOT 2
- Bug: 'unterminated comment' error when you have `/-` in a docstring HOT 2
- RFC: Use emoji variant selector for unicode characters HOT 4
- RFC: global diagnostics HOT 4
- Hovering over the `_` in `?_` shows irrelevant docstring
- `rw [def]` only works with first applicable equation lemma HOT 1
- default termination tactic: array_dec_dec tactic too eager, and too weak HOT 1
- bug: metavariable context being rolled back in simp
- typeclass inference crashes HOT 2
- Regression in inferring universe levels between v4.9.1 and v4.10.0-rc1 HOT 1
- decreasing_by goal with nested recursion mentions internal induction hypothesis
- RFC: remove `simpCtorEq` from the default simprocs HOT 1
- Broken Lake linking
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from lean4.