leanprover-community / lean-auto

Experiments in automation for Lean
Apache License 2.0
75 stars 12 forks source link

Fix string-format in warning for inductive types #18

Closed dranov closed 9 months ago

dranov commented 9 months ago

This printed the fixed string "{tyctor}". The formatting syntax works by default following trace, but not in the context of (_ ++ _).

PratherConid commented 9 months ago

Thanks! I think the trace environment is equivalent to m! instead of s!, so I changed the s! ro m!. It doesn't make much difference in this case though.