Command terminator

Stream: lean4

[Gabriel Ebner]

In Lean 3, you could terminate a command with a dot (e.g. if you wanted to use a user command right after you've defined it). Is there something similar in Lean 4? Or in other words, is there a nicer way to write the following?

local macro "ofNat_class" Class:ident n:num : command =>
  let field := Lean.mkIdent <| Class.getId.eraseMacroScopes.getString!.toLower
  `(class $Class:ident.{u} (α : Type u) where
    $field:ident : α

  instance {α} [$Class α] : OfNat α (nat_lit $n) where
    ofNat := ‹$Class α›.1

  instance {α} [OfNat α (nat_lit $n)] : $Class α where
    $field:ident := $n)

example : Nat := 0 -- terminate macro command

ofNat_class Zero 0

[Sebastian Ullrich]

We'll probably want indentation sensitivity for macro and syntax

[Leonardo de Moura]

@Sebastian Ullrich Yeah, I think indetation sensitivity is the way to go here.

[Leonardo de Moura]

@Gabriel Ebner Pushed the fix for this issue.