chore: move tests from Localization.v

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Sep 3, 2023 · a0a91bd · a0a91bd
1 parent 694b8d7
commit a0a91bd
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 9 deletions.
diff --git a/test/Modalities/Localization.v b/test/Modalities/Localization.v
@@ -0,0 +1,12 @@
+From HoTT.Modalities Require Import Localization.
+
+(** [ExtendableAlong_Over] takes 5 universe parameters:
+    - size of A
+    - size of B
+    - size of C
+    - size of D
+    - size of result (>= A,B,C,D) *)
+Check ExtendableAlong_Over@{a b c d m}.
+
+(** Universe parameters are the same as for [ExtendableAlong_Over]. *)
+Check ooExtendableAlong_Over@{a b c d m}.
diff --git a/theories/Modalities/Localization.v b/theories/Modalities/Localization.v
@@ -63,13 +63,6 @@ Fixpoint ExtendableAlong_Over@{a b c d m}
                   ExtendableAlong_Over n f (fun b => h b = k b)
                     (fun b c => c # h' b = k' b) (snd ext' h k)
      end ext.
-Check ExtendableAlong_Over@{a b c d m}.
-(** [ExtendableAlong_Over] takes 5 universe parameters:
-    - size of A
-    - size of B
-    - size of C
-    - size of D
-    - size of result (>= A,B,C,D) *)
 
 (** Like [ExtendableAlong], these can be postcomposed with known equivalences. *)
 Definition extendable_over_postcompose' (n : nat)
@@ -163,8 +156,6 @@ Definition ooExtendableAlong_Over
          {A B : Type} (f : A -> B) (C : B -> Type)
          (D : forall b, C b -> Type) (ext : ooExtendableAlong f C)
   := forall n, ExtendableAlong_Over n f C D (ext n).
-(** Universe parameters are the same as for [ExtendableAlong_Over]. *)
-Check ooExtendableAlong_Over@{a b c d r}.
 
 (** The [oo]-version for trivial dependency. *)
 Definition ooextendable_over_const