Zulip Chat Archive

Stream: new members

Topic: Anton Mellit

Anton Mellit (Dec 18 2023 at 10:42):

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 (Dec 18 2023 at 10:43):

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

Ruben Van de Velde (Dec 18 2023 at 10:44):

Also on simp getting weaker recently

Kevin Buzzard (Dec 18 2023 at 10:44):

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 (Dec 18 2023 at 10:45):

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

Anton Mellit (Dec 18 2023 at 10:48):


Martin Dvořák (Dec 18 2023 at 13:21):

Please also post to
so that I don't feel so alone here.

David Loeffler (Dec 19 2023 at 11:19):

Hi Anton, welcome on board!

Last updated: Dec 20 2023 at 11:08 UTC