mirror of
https://github.com/luau-lang/luau.git
synced 2024-11-15 22:35:43 +08:00
0bd21762ae
Prototypes booleans and relational operators. As part of this I removed `FFI/Data/Bool.agda`, because it was getting in the way - we already use `Agda.Builtin.Bool` instead for other cases.
17 lines
287 B
Agda
17 lines
287 B
Agda
module Utility.Bool where
|
|
|
|
open import Agda.Builtin.Bool using (Bool; true; false)
|
|
|
|
not : Bool → Bool
|
|
not false = true
|
|
not true = false
|
|
|
|
_or_ : Bool → Bool → Bool
|
|
true or _ = true
|
|
_ or true = true
|
|
_ or _ = false
|
|
|
|
_and_ : Bool → Bool → Bool
|
|
true and true = true
|
|
_ and _ = false
|