Repository navigation
v0.0.17
feat: improve json% syntax See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/json.20elaborator.
feat: improve json% syntax See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/json.20elaborator.