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

Trying to get it to compile with Agda 2.6.0

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-07 18:10:13 -06:00
parent e86b9772c8
commit 33ba6b0e3f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
prototyping/Luau/Syntax/FromJSON.agda
View file

@ -14,7 +14,7 @@ open import FFI.Data.Vector using (head; tail; null; empty)
args = fromString "args"
body = fromString "body"
func = fromString "func"
local = fromString "local"
lokal = fromString "local"
list = fromString "list"
name = fromString "name"
type = fromString "type"
@ -62,7 +62,7 @@ exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just v
exprFromObject obj | just (string "AstExprFunction") | just _ | just _ = Left "AstExprFunction args not an array"
exprFromObject obj | just (string "AstExprFunction") | nothing | _ = Left "AstExprFunction missing args"
exprFromObject obj | just (string "AstExprFunction") | _ | nothing = Left "AstExprFunction missing body"
exprFromObject obj | just (string "AstExprLocal") with lookup local obj
exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj
exprFromObject obj | just (string "AstExprLocal") | just (string x) = Right (var x)
exprFromObject obj | just (string "AstExprLocal") | just (_) = Left "AstExprLocal local not a string"
exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"