Add do notation

[janmasrovira]

• Closes Add do-notation #2355
• Depends on Register builtins during scoping and report proper errors instead of crashing #2943

Example:

minusOne : Nat -> Maybe Nat
  | zero := nothing
  | (suc n) := just n;


minusThree (n : Nat) : Maybe Nat :=
  do {
    x1 <- minusOne n;
    x2 <- minusOne x1;
    let
      x2' : Nat := x2;
    in
    x3 <- minusOne x2';
    pure x3;
  };

[paulcadman]

🌯