Remove allow unused metas

This commit is contained in:
Michael Zhang 2024-06-29 14:53:45 -05:00
parent 83ceb81f8a
commit 9318880a9a

View file

@ -24,7 +24,6 @@ $$
<small>The following line imports some of the definitions used in this post.</small>
```
{-# OPTIONS --allow-unsolved-metas #-}
open import Prelude
open Σ
```