Function that takes a pair

Stream: new members

[Iocta]

I'm getting started. The tutorial wants me to write a function def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := sorry but I'm not sure the syntax for writing a function that it would take as an argument.

I tried

def g : ℕ  ×  ℕ ->  ℕ := λ x y, x + y
#eval g (5, 3)

but it doesn't seem to like that: "failed to synthesize type class instance".

[YH]

def g : ℕ  ×  ℕ ->  ℕ := λ ⟨x, y⟩, x + y
#eval g (5, 3)

[Iocta]

Thanks.

[Kevin Buzzard]

YH's trick used to confuse me when I was beginning. It's a clever and important trick, but you can also do this:

def g : ℕ  ×  ℕ ->  ℕ := λ xy, xy.1 + xy.2

[Kevin Buzzard]

Either way, the point is that ℕ × ℕ is one type, so λ x y, can't be the way to start. That's why you got the error.

[Kevin Buzzard]

As a professional mathematician who knew essentially nothing about functional programming when I started, I took a while to get the hang of all this basic stuff; on the other hand computer science undergraduates with a Haskell background find the whole thing trivial.

[Iocta]

I see. I am checking out Lean after watching your recent talk on youtube. :-)

[Kevin Buzzard]

Great! When you're finished with Theorem Proving In Lean you could try the natural number game

[Bryan Gin-ge Chen]

A while back as a demo for some other stuff, I made a little interactive walkthrough about currying and uncurrying in Lean. Not sure if it's pitched at the right level (it assumes that you're OK with Lean's basic syntax), but you might find it helpful nonetheless.

[Johan Commelin]

Whoow! @Bryan Gin-ge Chen That's really fantastic! The way you walk through interactively writing the code, see the tactic state (and expected types), and have your explanation right below. Really really great!

[Kevin Buzzard]

What does

To use it yourself, add footer: stepEditor(steps, index) to the options object of leanEditor, where steps is an array of objects (see below) and index (optional, set to 0 by default) is the starting index.

mean? I am reading it as meaning "before you go any further, change an option in a place which you don't understand (the "options object of leanEditor").

[Bryan Gin-ge Chen]

Sorry, those are instructions for people who would want to use this function in another Observable notebook. I ought to to make that more clear.

[Kevin Buzzard]

Bryan I would happily promote these little notebooks on Twitter. I have followers who are in to little "gimmicky" stuff like this. Maybe you should send me a random list of cool little things you've done and I can shout them out. I still have under 1000 followers but it slowly goes up and I'm trying to figure out what works well in the ecosystem there; I suspect that this stuff might.

[Bryan Gin-ge Chen]

Thanks Kevin, feel free to share any or all of the notebooks in this "collection". @Kevin Kappelmann also has several neat tools / templates for Lean notebooks here.

I haven't had much time for Twitter recently, but my account is here. To be honest, at the moment I'd prefer to fix up my notebooks a bit more before making any kind of publicity push, as there are still lots of things I could do to make the editor more user friendly.

[Kevin Buzzard]

In the walkthrough linked to above, why not (a) delete all the stuff about how you made it and just make it a stand-alone thing with a link to a "how I did it" page, and (b) add a 15th page with the formalised sorried examples such as uncurry add' = add and curry uncurry = idso the user doesn't have to figure out how to formalise the statements? If they're interested they will figure out some more questions on their own after they've done the easier job of filling in the sorrys

[Bryan Gin-ge Chen]

Great suggestions! I'll try to implement them soon.