Anton Mellit

Stream: new members

[Anton Mellit]

Hi all! I'm at University of Vienna, doing mostly algebraic geometry, rep. theory and combinatorics. I like coding and computer experiments, so I'm curious about Lean.

I'm going through "Functional Programming in Lean" and got stuck at proving that 3<5. According to the book "by simp" should work, but it doesn't! On the other hand I tried "by trivial" and it worked. Is it expected and the book is wrong or is it a bug?

[Kevin Buzzard]

This might depend on (a) imports and (b) which 3 you're talking about :-)

[Ruben Van de Velde]

Also on simp getting weaker recently

[Kevin Buzzard]

Oh yes that will be it. simp used to try decide but now it doesn't. So indeed the book is out of date.

example : (3 : Nat) < 5 := by decide

[Anton Mellit]

I don't have any imports. I tried refining to (3:Nat)<(5:Nat), it didn't change anything

[Anton Mellit]

thanks!

[Martin Dvořák]

Please also post to
https://leanprover.zulipchat.com/#narrow/stream/224796-Geographic-locality/topic/Vienna.2C.20AT
so that I don't feel so alone here.

[David Loeffler]

Hi Anton, welcome on board!