tutorial
tutorial copied to clipboard
leanprover
Lean Tutorials
The first "Try it yourself example" of the chapter "4 Quantifiers and Equality" won't compile and throws the error `Unknown identifier 'take'` using Lean 3.28. I guess there should be...
There is at least one snippets that does not work with the current lean 2 version, in `10_Structures_and_Records.org`: ```lean import standard open nat structure big := (field1 : nat) (field2...
Add how dependent pattern matching works for anonymous `have` expressions and `show` expressions (the inductive definition is called `this`).
Just leaving this issue here as a reminder for the TODO in the text (from aaa36e6 on Dec 30, 2014).
I'm listing several bugs here, but they all have the same root cause and fix, related to how internal links are handled. Bug 1: from https://leanprover.github.io/tutorial/index.html, I click the drop-down...
