Skip to content

Commit

Permalink
Merge pull request #18 from dranov/tyctor-warning
Browse files Browse the repository at this point in the history
Fix string-format in warning for inductive types
  • Loading branch information
PratherConid authored Feb 15, 2024
2 parents e0e3d67 + 1f78265 commit abbe4b3
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Auto/Translation/Inductive.lean
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ mutual
let .some (.inductInfo val) := (← getEnv).find? tyctor
| return
if !(← @id (CoreM _) (val.all.allM isSimpleInductive)) then
trace[auto.collectInd] ("Warning : {tyctor} or some type within the " ++
trace[auto.collectInd] (m!"Warning : {tyctor} or some type within the " ++
"same mutual block is not a simple inductive type. Ignoring it ...")
return
/-
Expand Down

0 comments on commit abbe4b3

Please sign in to comment.