Syntax wrangling

Stream: lean4

[Patrick Massot]

I'm mostly done porting Verbose Lean to Lean 4 and I would like to experiment with also changing the syntax to define exercises. I naively tried the following

import Lean

open Lean Meta Elab Command

def explBinder := leading_parser Lean.Parser.Term.explicitBinder

open TSyntax.Compat in
def mkExampleArgs (objs hyps : TSyntaxArray `explBinder)  :
    TSyntaxArray `Lean.Parser.Term.bracketedBinder :=
  objs ++ hyps


elab "Exercise" str "Given:" objs:explBinder* "Assume:" hyps:explBinder* "Conclusion:" concl:term "Proof:" prf:tacticSeq : command => do
  elabCommand (← `(command|example $(mkExampleArgs objs hyps):bracketedBinder* : $concl := by $prf))

set_option pp.rawOnError true

Exercise "Test"
  Given: (n : Nat)
  Assume: (hn : n = 0)
  Conclusion: True

  Proof:
  trivial

You can see from open TSyntax.Compat in that I forced Lean a bit, and of course it didn't like it. I'd be grateful if anyone could tell me how to fix this attempt.

[Patrick Massot]

In case this isn't clear, in the failing example the command is meant to transcribe to example (n : Nat) (hn : n = 0) : True := by trivial.

[Mario Carneiro]

Why did you even define explBinder here, if it's just a wrapper around bracketedBinder? It works if you just remove that

open Lean.Parser.Term (bracketedBinder)

elab "Exercise" str
    "Given:" objs:bracketedBinder*
    "Assume:" hyps:bracketedBinder*
    "Conclusion:" concl:term
    "Proof:" prf:tacticSeq : command => do
  elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := by $prf))

[Patrick Massot]

I tried many variations, that's why.

[Patrick Massot]

Thanks!

[Patrick Massot]

However I would also like to experiment with variations so I guess this baby version was too easy. Say for instance I want to allow

Exercise "Test"
  Given:
    n : Nat
    p : Nat
  Assume: (hn : n = 0)
  Conclusion: True

  Proof:
  trivial

where each object is on its own line. Do you know how to do that?