create syntax with newline

Stream: lean4

[Tomas Skrivan]

How do I create a piece of syntax with newline? I want to create this `(let' $x ~ $y; $b) but with newline instead of semicolon.

I understand that anti-quotation strips all whitespace. Can I just somehow replace the semicolon with newline? I tried this but it does not work (btw I have no idea what I'm doing here so it is not surprising it does not work)

partial def _root_.Lean.Syntax.semicolonToNewline : Syntax → Syntax
| .node info kind args => .node info kind (args.map fun s => semicolonToNewline s)
| .atom info val => if val == ";" then .atom info "\n" else .atom info val
| s => s

mwe

import Lean

open Lean

def bind' (x : α) (f : α → β) : β := f x

open Lean.Parser
macro "let'" x:term " ~ " y:term semicolonOrLinebreak b:term : term => `(bind' $y (fun $x => $b))

@[app_unexpander bind'] def unexpandBind' : Lean.PrettyPrinter.Unexpander

| `($(_) $y $f) =>
  match f with
  | `(fun $x:term => $b) =>
    `(let' $x ~ $y; $b) -- how do I create this with new line?
  | _ => `(let' x ~ $y; $f x)

| _ => throw ()

/-
let' x ~ 10;x + x : Nat
-/
#check let' x ~ 10; x + x

How do I make #check let' x ~ 10; x + x to print out?

let' x ~ 10
x + x : Nat

[Mario Carneiro]

you can just put a literal newline in the quotation

[Tomas Skrivan]

And how do I do that?

This does not work

let n := mkStrLit "\n"
`(let' $x ~ $y $n $b)

[Mario Carneiro]

you put an actual newline in

[Mario Carneiro]

`(let' $x ~ $y
  $b)

[Tomas Skrivan]

That does not print out the newline back.

[Mario Carneiro]

import Lean

open Lean

def bind' (x : α) (f : α → β) : β := f x

open Lean.Parser
syntax withPosition("let'" term " ~ " term semicolonOrLinebreak ppDedent(ppLine) term) : term
macro_rules
  | `(let' $x ~ $y; $b) => `(bind' $y (fun $x => $b))

@[app_unexpander bind'] def unexpandBind' : Lean.PrettyPrinter.Unexpander

| `($(_) $y $f) =>
  match f with
  | `(fun $x:term => $b) =>
    `(let' $x ~ $y
      $b)
  | _ =>
    `(let' x ~ $y
      $f x)

| _ => throw ()

/-
let' x ~ 10
x + x : Nat
-/
#check let' x ~ 10
       x + x

[Tomas Skrivan]

Thanks! I see I missed ppLine in the syntax definition.