lean-training-data icon indicating copy to clipboard operation
lean-training-data copied to clipboard
verified publisher icon semorrison

`goal_comments`has no effect

Open zzhisthebest opened this issue 8 months ago • 1 comments

I tried lake exe goal_comments Mathlib.Logic.Hydra and lake exe goal_comments Mathlib.Logic.Hydra --edit, but the -- ⊢ x = y aren't inserted at all.

zzhisthebest avatar Mar 28 '25 03:03 zzhisthebest