This repository has been archived by the owner on May 17, 2024. It is now read-only.

About Equal.refl #76

Open

iacore opened this issue Nov 1, 2022 · 0 comments

iacore commented Nov 1, 2022

If I understand the code correctly, in Kind2, Equal.refl is not a constructor, but a regular definition.

This may be problematic, where inductive constructors are injective, while normal definitions may not be

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.