From 15a48a0cef54c9e31c23f542fdc09c7480622997 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 21 Apr 2022 15:26:42 -0500 Subject: [PATCH] WIP --- prototyping/Properties/Subtyping.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index 4c1be220..4225491b 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -1,5 +1,5 @@ {-# OPTIONS --rewriting #-} -{-# OPTIONS --allow-unsolved-metas #-} + module Properties.Subtyping where open import Agda.Builtin.Equality using (_≡_; refl)