search

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
54 stars 13 forks source link

fix: NameGenerator bug #32

Closed semorrison closed 5 months ago

semorrison commented 5 months ago

This is probably not the long-term fix; I need to understand how NameGenerator is intended to be plumbed. However this fixes an observed problem in the meantime.