From 0bb7cd9632c25cbe5b0c8610045a979c966f4918 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 8 Feb 2022 11:17:42 -0600 Subject: [PATCH] Get examples to typecheck again --- prototyping/Examples/Syntax.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prototyping/Examples/Syntax.agda b/prototyping/Examples/Syntax.agda index b6e57cf5..d16dfebb 100644 --- a/prototyping/Examples/Syntax.agda +++ b/prototyping/Examples/Syntax.agda @@ -17,7 +17,7 @@ ex2 : blockToString(return nil ∙) ≡ ex2 = refl ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ end ∙ return f ∙) ≡ - "function f(x)\n" ++ + "local function f(x)\n" ++ " return x\n" ++ "end\n" ++ "return f"