Zulip Chat Archive

Stream: new members

Topic: simple pattern matching with lean4


view this post on Zulip 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"
term
  "a"
has type
  String
but is expected to have type
  Int
$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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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?

view this post on Zulip 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)?

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Sep 28 2019 at 22:03):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 29 2019 at 10:27):

have you ever read agda code?

view this post on Zulip Mario Carneiro (Sep 29 2019 at 10:27):

unicode can be overused

view this post on Zulip Marc Huisinga (Sep 29 2019 at 10:34):

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

view this post on Zulip Marc Huisinga (Sep 29 2019 at 10:36):

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

view this post on Zulip Patrick Massot (Sep 29 2019 at 10:37):

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

view this post on Zulip Mario Carneiro (Sep 29 2019 at 10:37):

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

view this post on Zulip Patrick Massot (Sep 29 2019 at 10:38):

You can define functions in math

view this post on Zulip Mario Carneiro (Sep 29 2019 at 10:38):

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

view this post on Zulip Mario Carneiro (Sep 29 2019 at 10:39):

by programmy stuff I mean lean core

view this post on Zulip 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: May 14 2021 at 21:11 UTC