Zulip Chat Archive

Stream: new members

Topic: notation of def doesn't show types clearly


Robert Watson (Feb 05 2022 at 16:11):

Hi all. Is there any way of getting the following (Agda-like) notation so as to make Lean more intuitive for dealing with type-level programming. Instead of: def myfunc (z : ℤ) : ℤ := z, The Type would be made explicit with the following (or similar):

dfn myfunc' : ℤ → ℤ :=
myfunc' z = z

(obviously with some sort of compatible notation for square and squiggly brackets)

Is anything like this available?

Alex J. Best (Feb 05 2022 at 16:16):

You can use a pattern match (known also as the equation compiler)

def myfunc' :   
| z := z

I don't know how to use squigly brackets with it though

Alex J. Best (Feb 05 2022 at 16:17):

You could do

def myfunc' {z : } :  :=
match z with
| z := z
end

for squigly brackets but that kinda defeats the point in this example

Robert Watson (Feb 05 2022 at 16:24):

Looks perfect. Thanks. In case any other noob is interested, you can then do something like this no problem:

def myfunc2' : nat → ℤ | nat.zero := int.zero | (nat.succ n) := int.one

Anne Baanen (Feb 07 2022 at 10:55):

Alex J. Best said:

You can use a pattern match (known also as the equation compiler)

def myfunc' :   
| z := z

I don't know how to use squigly brackets with it though

For what it's worth, here's how to do so:

def myfunc' : Π {z : }, 
| z := z

Last updated: Dec 20 2023 at 11:08 UTC