mirror of
https://github.com/luau-lang/luau.git
synced 2024-12-13 21:40:43 +00: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.
20 lines
529 B
Agda
20 lines
529 B
Agda
module Luau.Value where
|
|
|
|
open import Agda.Builtin.Bool using (Bool; true; false)
|
|
open import Agda.Builtin.Float using (Float)
|
|
open import Luau.Addr using (Addr)
|
|
open import Luau.Syntax using (Block; Expr; nil; addr; number; true; false)
|
|
open import Luau.Var using (Var)
|
|
|
|
data Value : Set where
|
|
nil : Value
|
|
addr : Addr → Value
|
|
number : Float → Value
|
|
bool : Bool → Value
|
|
|
|
val : ∀ {a} → Value → Expr a
|
|
val nil = nil
|
|
val (addr a) = addr a
|
|
val (number x) = number x
|
|
val (bool false) = false
|
|
val (bool true) = true
|