notation of def doesn't show types clearly

Stream: new members

[Robert Watson]

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]

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]

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]

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]

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