Commit 2020-04-18 15:15 4e872238
View on Github →feat(tactic/transport): transport structures across equivalences (#2251)
Blocked by #2246.
Blocked on #2319 and #2334, which both fix lower tactic layers used by transport.
From the doc-string:
transport.Given a goal ⊢ S β for some parametrized structure type S,
transport will look for a hypothesis s : S α and an equivalence e : α ≃ β,
and attempt to close the goal by transporting s across the equivalence e.
example {α : Type} [ring α] {β : Type} (e : α ≃ β) : ring β :=
by transport.
You can specify the object to transport using transport s,
and the equivalence to transport across using transport s using e.
You can just as easily transport a semilattice_sup_top or a lie_ring.
In the test/transport.lean file we transport semiring from nat to mynat, and verify that it's possible to do simple things with the transported structure.