Stream: Coq users

Topic: path_indution tactic in HoTT


view this post on Zulip Callan McGill (Mar 05 2022 at 05:59):

Do any of you know anywhere that explains how the path_induction tactic of the HoTT library works?

view this post on Zulip Ali Caglayan (Mar 07 2022 at 01:51):

Well I wouldn't really use the path_induction tactic in practice. All it is doing is calling destruct on a path in the context. First it introduces all the variables it can, then it looks for any variables of the path type, if it has found some it tries induction (which is really just destruct since there is no IH). I think you are better off calling destruct on your path hypotheses yourself.

view this post on Zulip Ali Caglayan (Mar 07 2022 at 01:53):

By the way there is a HoTT zulip if you are interested: https://hott.zulipchat.com/


Last updated: Jan 29 2023 at 01:02 UTC