Skip to content

Commit

Permalink
replace cast_trans with cast_cast
Browse files Browse the repository at this point in the history
  • Loading branch information
alexkeizer committed Dec 18, 2024
1 parent 8c4bb8d commit da1cc33
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Qpf/Util/HEq.lean
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ syntax "simp_heq" optConfig (discharger)? ("only ")? ("[" simpLemma,* "]")? (loc
macro_rules
| `(tactic| simp_heq $cfg:optConfig $[$dis:discharger]? $[$loc:location]? )
=> `(tactic| simp $cfg $[$dis]?
only [cast_trans, heq_cast_left, heq_cast_right, cast_eq, cast_heq,
only [cast_cast, heq_cast_left, heq_cast_right, cast_eq, cast_heq,
heq_cast_left_fun, heq_cast_right_fun, cast_arg', HEq.refl]
$[$loc]?
)
Expand Down

0 comments on commit da1cc33

Please sign in to comment.