ketilwright

The blue box states a different problem than the example. In the blue box, you have {n:Z s.t. n = 1 zmod 5} intersected with {n:N s.t. n = 1...

There is a theorem gcd_dvd starting about line 60 of this file. It's not clear if the reader should resolve the 8 sorries or not. I think not since gcd_dvd_right...

recursion depth problem in chapter 7 examples

3

These examples in Chapter 7, Inductive Types raise recursion depth errors: ``` namespace Hidden theorem add_zero (n : Nat) : n + 0 = n := Nat.add_zero n open Nat...

Hypotheses as variables not available in theorems with lean 4.12

4

After updating from lean 4.8 to 4.12, I found it necessary to change some of the examples in Chapter 4 (Quantifiers and Equality) There are many problems reported here: variable...

This proof squiggles on add_succ succ_add ``` def replicate (n : Nat) (a : α) : List α := loop n [] where loop : Nat → List α →...

Following the Vector tailAux function > The difficulty in defining tail is to maintain the relationships between the indices. The hypothesis e : m = n + 1 in tailAux...

Chapter 8: the text says eval will work even though natToBin has a sorry. It doesn't.

This example generates errors ``` example (x y : Nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y +...

Broken length_replicate proof (chapter 8)

1

In the "Induction and Recursion" chapter, the last proof in "Local recursive declaration" doesn't work: ``` theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n...

This generates "compile" errors ``` namespace Hidden theorem subst {α : Type u} {a b : α} {p : α → Prop} (h₁ : Eq a b) (h₂ : p...