New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Uniform ticks for sub/supertypes #7

Open

0xd34df00d opened this issue May 30, 2022 · 0 comments

Assignees

Labels

Owner

0xd34df00d commented May 30, 2022

Let's have a convention that subtype is always ticked and supertype is always unticked, along the lines of

  ST-Arr  : [ θ ] Γ ⊢ τ₁' <: τ₁
          → [ θ ] Γ , τ₁' ⊢ τ₂' <: τ₂
          → [ θ ] Γ ⊢ τ₁ ⇒ τ₂'
          → [ θ ] Γ ⊢ τ₁'
          → [ θ ] Γ ⊢ τ₁ ⇒ τ₂' <: τ₁' ⇒ τ₂

Otherwise dealing with holes around subtypes is a terrible mess.

0xd34df00d added the presentation label

0xd34df00d self-assigned this

0xd34df00d changed the title ~~Uniform ticks for sub/supertypese~~ Uniform ticks for sub/supertypes

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