Skip to content

Commit

Permalink
chore: fix test
Browse files Browse the repository at this point in the history
  • Loading branch information
@leodemoura
leodemoura committed Feb 2, 2025
1 parent b0a4859 commit 8350895
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions tests/lean/run/prelude-injectivity.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ gen_injective_theorems% Macro.State
gen_injective_theorems% Syntax.Preresolved
gen_injective_theorems% Syntax.SepArray
gen_injective_theorems% Syntax.TSepArray
gen_injective_theorems% Try.Config
gen_injective_theorems% Parser.Tactic.DecideConfig
-/
#guard_msgs in
Expand Down

0 comments on commit 8350895

Please sign in to comment.