ketilwright comments

Repositories
Issues
Comments

Results 4 comments of


                                            ketilwright

recursion depth problem in chapter 7 examples

Lean (version 4.12.0, x86_64-apple-darwin22.6.0, commit dc2533473114, Release)

Broken length_replicate proof (chapter 8)

lean --version says Lean (version 4.12.0, x86_64-apple-darwin22.6.0, commit dc2533473114, Release)

Hypotheses as variables not available in theorems with lean 4.12

Another example is in the following chapter: ``` variable (g : Nat → Nat → Nat) variable (hg : g 0 0 = 0) theorem gex1 : ∃ x, g...

Hypotheses as variables not available in theorems with lean 4.12

I suppose I closed it once I understood this particular problem. I suspect this is just an example of a more general problem with TPIL, which doesn't appear to have...