luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

Oops, forgot a hole!

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-03-25 14:22:12 -05:00
parent afe4700d59
commit 4a0ad2e025
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
prototyping/Properties/Subtyping.agda
View file

@ -265,7 +265,7 @@ not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →
(∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) → Q ⊆ Comp((Language S₂) ⊗ Comp(Language T₂))) →
(Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂))
not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = {!!} where
not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = r where
Q : (Tree × Tree) → Set
Q (t , u) = Either (¬Language S₁ t) (Language T₁ u)