| def four1 := double 2 | |
| where double (n : Nat) : Nat := 2 * n | |
| def four2 := double 2 | |
| where double : Nat → Nat := fun n => 2 * n | |
| def four3 := double 2 | |
| where double(n : Nat) : Nat := 2 * n | |
| def four4 := double 2 | |
| where double: Nat → Nat := fun n => 2 * n | |
| def four5 := let double(n : Nat) : Nat := 2 * n | |
| double 2 | |
| def four6 := let double: Nat → Nat := fun n => 2 * n | |
| double 2 | |
| def four7 := let rec double: Nat → Nat := fun n => 2 * n | |
| double 2 |