custom syntax

Stream: metaprogramming / tactics

[Adem Bizid]

I was wondering if one can make some function that is able to generate random instance of some custom syntax. For instance a list comprehension; how can I create a function that generates random instances of the following definition of list comprehension

import Lean

open Lean Elab Command Meta

/-- List comprehension syntax. -/
syntax (name := listComprehension) "[" term "|" term " in " term (" if " term)? "]" : term

macro_rules
  | `([ $expr | $item in $items if $predicate ]) =>
      `(List.map (fun $item => $expr) (List.filter (fun $item => $predicate) $items))
  | `([ $expr | $item in $items ]) =>
      `(List.map (fun $item => $expr) $items)

[Aaron Liu]

Do you have an informal implementation?

[Adem Bizid]

Define a distribution over the instances of the syntax implicitly and than sample from it.

[Alok Singh]

I'm also interested in this but also unsure of next step. Best I've come up with so far is to wire up Lean.Expr with plausible, but that's not code.