leanprover theorem_proving_in_lean4 issues

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4

https://leanprover.github.io/theorem_proving_in_lean4/

Apache License 2.0

164 stars 92 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

#eval natToBin 123456 should be #eval!

#140 ketilwright opened 1 day ago
0
Broken div example proof chapter 8

#139 ketilwright opened 1 day ago
0
Broken length_replicate proof (chapter 8)

#138 ketilwright opened 2 days ago
1
Explanation of what a structure is

#137 hrmacbeth opened 3 weeks ago
0
Error in 2nd subst example

#136 ketilwright opened 3 weeks ago
0
Deletes repeated section Local Recursive Definitions in induction_and_recursion.md

#135 javierlcontreras opened 3 weeks ago
0
recursion depth problem in chapter 7 examples

#134 ketilwright opened 3 weeks ago
1
Use eval! to evaluate functions that use sorry.

#133 lcrh opened 1 month ago
1
`mutual` is not highlighted

#132 seanmcl opened 1 month ago
0
Error "unknown identifier 'hp'" in chapter 3 "Propositions and Proofs" when using `variable (hp: p)`

#131 MichaelJFishman opened 1 month ago
1
Hypotheses as variables not available in theorems with lean 4.12

#130 ketilwright closed 1 month ago
1
PDF version

#129 projetmbc opened 2 months ago
0
add: Table of Contents to each chapter (2-12) using `mdbook-toc`

#128 thelissimus opened 2 months ago
0
Ch. 6 "Using the Library" link broken

#127 Morgan-Sinclaire opened 3 months ago
0
These 2 sentences in Ch. 7 are a holdover from Lean3

#126 Morgan-Sinclaire opened 3 months ago
0
This should be capital True I think

#125 johnmwu opened 3 months ago
0
fix: update stale lean 4 extension instructions

#124 mhuisi closed 1 month ago
0
remove redundant section

#123 williamdemeo closed 4 months ago
1
small but unpleasant typo

#122 stepanholub opened 4 months ago
0
compound repeat first tactic no longer solves all three permutations of `\and` propositions

#121 jordane95 opened 4 months ago
0
Examples in Inductive Types chapter broken due to `simp_eq_add_one` simp rule

#120 avigad opened 5 months ago
0
add pdf version and build instructions

#119 ocramz opened 5 months ago
0
Update Std -> Batteries

#118 Timeroot closed 4 months ago
0
fix: clarify that Lean's core library uses classical logic

#117 avigad opened 6 months ago
0
Propositions and currying

#116 DavidPratten opened 6 months ago
0
Duplicate section on Local recursive declarations

#115 solleks opened 6 months ago
0
Suggestions for clarity

#114 turibe opened 6 months ago
3
Small typos and formatting

#113 turibe closed 6 months ago
0
Small fixes

#112 turibe closed 6 months ago
3
ambiguous, possible interpretations on sample code in Quantifiers and Equality chapter

#111 trj2059 opened 7 months ago
0
doc: clarify how Lean supports constructive logic

#110 chabulhwi closed 4 months ago
2
Some graphics missing in VSCodium

#109 navidrashidian opened 8 months ago
2
Fix: ambiguity with newly introduced divisibility symbol

#108 MatteoGaetzner opened 8 months ago
1
fix: Update examples to work with latest Lean nightly

#107 david-christiansen opened 8 months ago
1
Fixed typo

#106 MatteoGaetzner closed 8 months ago
1
The theme changes when I click on the print icon

#105 xiaoxi-david opened 9 months ago
0
Theorem for ¬(p ↔ ¬p) missing?

#104 MatteoGaetzner closed 8 months ago
4
Link to Quickstart instead of Setup on title page

#103 avigad closed 8 months ago
1
fix: restore link to old URL for TPiL3

#102 david-christiansen closed 9 months ago
0
fix: update link domains to lean-lang.org

#101 david-christiansen closed 9 months ago
0
auto bound implicit args are not limited to single letters

#100 medovina opened 9 months ago
1
Update type_classes.md

#99 Ritterbeck closed 10 months ago
1
fix: update links to new domain

#98 david-christiansen closed 10 months ago
0
fix: replace placeholder link with FPiL

#97 david-christiansen closed 10 months ago
0
Fix confusion in quantifiers_and_equality.md

#96 AmourAmer closed 10 months ago
2
chore: update to new termination_by syntax

#95 nomeata closed 10 months ago
0
Remove duplicated section.

#94 DeVilhena-Paulo opened 10 months ago
0
chore: add Netlify deployment

#93 david-christiansen closed 10 months ago
0
Implement a button to jump to the Lean Web Editor

#92 Seasawher closed 7 months ago
0
provide a table of contents

#91 Seasawher closed 7 months ago
0