../

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.

  • You cannot do two print statement without a do block

  • do block does some funky monad stuff

  • But essentially it allows you write procedural like code. But it is not actually procedural

  • It is more like composition