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

Apply suggestions from code review

Browse source 
Co-authored-by: Lily Brown <lily@lily.fyi>
This commit is contained in:
Alan Jeffrey 2022-03-02 13:17:13 -06:00 • committed by GitHub
parent 70348e728b
commit 4fb0d28e23
Signed by: DevComp
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
prototyping/Luau/OpSem.agda
View file

@ -23,12 +23,8 @@ evalEqOp (bool false) (bool y) = not y
evalEqOp _ _ = false evalEqOp _ _ = false
evalNeqOp : Value → Value → Bool evalNeqOp : Value → Value → Bool
evalNeqOp Value.nil Value.nil = false
evalNeqOp (addr x) (addr y) = not (x ==ᴬ y)
evalNeqOp (number x) (number y) = primFloatInequality x y evalNeqOp (number x) (number y) = primFloatInequality x y
evalNeqOp (bool true) (bool y) = not y evalNeqOp x y = not (evalEqOp x y)
evalNeqOp (bool false) (bool y) = y
evalNeqOp _ _ = true
data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
+ : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n) + : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n)

2
prototyping/Luau/VarCtxt.agda
View file

@ -22,7 +22,7 @@ _⋓_ : VarCtxt → VarCtxt → VarCtxt
_⋓_ = unionWith _∪_ _⋓_ = unionWith _∪_
_[_] : VarCtxt → Var → Maybe Type _[_] : VarCtxt → Var → Maybe Type
_[_] Γ x = lookup (fromString x) Γ Γ [ x ] = lookup (fromString x) Γ
_⊝_ : VarCtxt → Var → VarCtxt _⊝_ : VarCtxt → Var → VarCtxt
Γ ⊝ x = delete (fromString x) Γ Γ ⊝ x = delete (fromString x) Γ