mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
21 lines
611 B
Agda
21 lines
611 B
Agda
module Examples.Type where
|
||
|
||
open import Agda.Builtin.Equality using (_≡_; refl)
|
||
open import FFI.Data.String using (_++_)
|
||
open import Luau.Type using (nil; _∪_; _∩_; _⇒_)
|
||
open import Luau.Type.ToString using (typeToString)
|
||
|
||
ex1 : typeToString(nil) ≡ "nil"
|
||
ex1 = refl
|
||
|
||
ex2 : typeToString(nil ⇒ nil) ≡ "(nil) -> nil"
|
||
ex2 = refl
|
||
|
||
ex3 : typeToString(nil ⇒ (nil ⇒ nil)) ≡ "(nil) -> (nil) -> nil"
|
||
ex3 = refl
|
||
|
||
ex4 : typeToString(nil ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> (nil) -> nil)?"
|
||
ex4 = refl
|
||
|
||
ex5 : typeToString(nil ⇒ ((nil ⇒ nil) ∪ nil)) ≡ "(nil) -> ((nil) -> nil)?"
|
||
ex5 = refl
|