From a0f4fbc68a91bc2bb64e7eb878d04ca776245db7 Mon Sep 17 00:00:00 2001 From: Ian Voysey Date: Mon, 31 Oct 2016 14:09:56 -0400 Subject: [PATCH] should have deleted arg when we took out construct arg, but i missed it. a reviewer for POPL-AE found it. --- core.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/core.agda b/core.agda index e3565c6..133bf2c 100644 --- a/core.agda +++ b/core.agda @@ -284,7 +284,6 @@ module core where var : Nat → shape lam : Nat → shape ap : shape - arg : shape numlit : Nat → shape plus : shape nehole : shape