../

Lean4

Function definition

There is no declaration here.

When I type def MyFunc: IO Unit, lean4 expects :=, where or |

  • := is to literally assign another term to this function
  • where
    • This is used for structs
  • | is to pattern match against the incoming args.