Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff OPair.agda @ 363:aad9249d1e8f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hω2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Jul 2020 10:36:32 +0900
parents 8a430df110eb
children 7f919d6b045b
line wrap: on
line diff
--- a/OPair.agda	Fri Jul 17 18:57:40 2020 +0900
+++ b/OPair.agda	Sat Jul 18 10:36:32 2020 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Level
 open import Ordinals
 module OPair {n : Level } (O : Ordinals {n})   where