## 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