Zulip Chat Archive

Stream: new members

Topic: simple pattern matching with lean4

Tobias Grosser (Sep 28 2019 at 14:20):

Hey guys (@Sebastian Ullrich?),

I am trying to get the following code to compile in lean4:

cat test.lean
import init.data.int.basic
import init.data.string.basic

def foo (ctx : String) : Int → Int
| x => if ctx == "a" then x else (foo "a" x)
$lean test.lean
/home/grosser/Projects/lean4/test.lean:4:4: error: type mismatch at application
  foo "a"
has type
but is expected to have type
$cat test2.lean
import init.data.int.basic
import init.data.string.basic

def foo : String → Int → Int
| "a" x => x
| _ x => foo "a" x
$lean test2.lean
/home/grosser/Projects/lean4/test2.lean:4:4: error: invalid application, function expected

The example is obviously artificial and reduced from an example that is a lot larger. What I want to do is -- in certain cases -- change the first argument and then recurse into the very same function with the updated first argument. Unfortunately, this does not seem to work. In the first test.lean file it seems ctx is already implicitly passed as the first argument to foo such that only the second argument can be passed to foo. In the second test case I get an error message which I do not fully understand. Any ideas?

Reid Barton (Sep 28 2019 at 15:43):

The first one is wrong in Lean 3 for the reason you say, I assume it is the same in Lean 4.
It looks like the second one needs commas in Lean 4, judging from (for example) https://github.com/leanprover/lean4/blob/master/library/init/data/list/basic.lean

Tobias Grosser (Sep 28 2019 at 18:02):

This seems to work. Thanks a lot. I should have looked myself a little deeper. I had the feeling I may have misunderstood sth basic, but it seems some syntax changed and the error message is not super descriptive. Thanks @Reid Barton for providing details here.

Kevin Buzzard (Sep 28 2019 at 18:17):

Wow, I hadn't really appreciated the following: that Lean 4 file (with all the CamelCase changes etc) still says copyright 2016 on it. Is that how it works? When mathlib gets ported we leave all the copyrights as they were -- they're not "new files"?

Patrick Massot (Sep 28 2019 at 20:16):

@Sebastian Ullrich will we keep that ASCII art =>? Or is it only used in core before the parser is able to handle a proper unicode arrow?

Patrick Massot (Sep 28 2019 at 20:17):

To all people who post Lean 4 code, do you understand correctly that there is still no VScode extension and you use Lean 4 non-interactively (or using emacs)?

Sebastian Ullrich (Sep 28 2019 at 22:01):

@Patrick Massot does already work. Leo seems to prefer the ASCII arrow, but we haven't really discussed coding styles so far (which of course we should do exactly once when implementing a standard code formatter for Lean 4 and then never talk about this topic again).

Mario Carneiro (Sep 28 2019 at 22:03):

wait, so the preference is unicode lambda + ascii arrow?

Sebastian Ullrich (Sep 29 2019 at 09:47):

No, Leo's current preference is fun + =>. My preference may be fun + but I haven't really decided yet.

Patrick Massot (Sep 29 2019 at 09:57):

Returning to ASCII would be really sad. Readable unicode is the first thing that attracts mathematicians to Lean after seeing Coq.

Mario Carneiro (Sep 29 2019 at 10:27):

have you ever read agda code?

Mario Carneiro (Sep 29 2019 at 10:27):

unicode can be overused

Marc Huisinga (Sep 29 2019 at 10:34):

is exchanging unicode for ascii the motivation for using fun instead of \lam as well?

Marc Huisinga (Sep 29 2019 at 10:36):

i suppose λ foo => bar would look a bit strange

Patrick Massot (Sep 29 2019 at 10:37):

This is no need to overuse unicode. We can keep words, but avoid ascii art.

Mario Carneiro (Sep 29 2019 at 10:37):

I like using ascii art for programmy stuff and unicode for math stuff

Patrick Massot (Sep 29 2019 at 10:38):

You can define functions in math

Mario Carneiro (Sep 29 2019 at 10:38):

I'm sure Scott and co will reserve all the arrows

Mario Carneiro (Sep 29 2019 at 10:39):

by programmy stuff I mean lean core

matt rice (Sep 30 2019 at 03:36):

Sometimes wish that the ascii -> unicode happened not in the editors input mechanism, but by running a pass over ASCII sources. So it would be represented as \lam foo, bar then converted to λ foo, bar for display... Not sure it'd be at all readable, but perhaps helpful if you weren't familiar with a symbol, but there are also tons of search boxes which are terrible at unicode... :shrug:

Last updated: Dec 20 2023 at 11:08 UTC