get default value

Stream: lean4

[Joseph O]

How can i get the default values of a type?

[Mario Carneiro]

The default function returns it, or you can peek at that type's Inhabited instance declaration

[Joseph O]

Then why does doing

#eval default Nat

give the error

function expected at
  default
term has type
  ?m.18

[Yakov Pechersky]

#eval (default : Nat)

[Yakov Pechersky]

default doesn't take the type as an explicit arg

[Joseph O]

ah