This repository has been archived by the owner on Sep 5, 2022. It is now read-only.

equivalence type #9

Closed

dannypsnl opened this issue Aug 16, 2021 · 0 comments

Assignees

Owner

dannypsnl commented Aug 16, 2021

The following program shows problem:

(data (≡ [a : A] [b : A]) : Type
      [refl : (≡ a a)])

(check (≡ z z)
       (refl))
(check (≡ z (s z))
       (refl))

Our unification didn't figure out this program has type mismatching.

dannypsnl changed the title ~~equaivlance type~~ equivalence type

dannypsnl self-assigned this

dannypsnl closed this as completed in

13ff465

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