[ #5000 ] testcases cosmetics #1428 #1292

We now have Agda.Builtin.Size !

test/Fail/Issue1428a.agda

@@ -1,32 +1,41 @@
 -- Andreas, 2015-03-16
+-- Andreas, 2020-10-26 removed loop during injectivity check
 
-open import Common.Size
-open import Common.Prelude
+open import Agda.Builtin.Size
 
 -- Note: the assumption of pred is absurd,
 -- but still should not make Agda loop.
 
 module _ (pred : ∀ i → Size< i) where
 
-data D (i : Size) : Set where
-  wrap : (j : Size< i) → D i
+data ⊥ : Set where
 
-loop : ∀ i → D i → ⊥
-loop i (wrap j) = loop j (wrap (pred j))
--- Loops during injectivity check
+data SizeLt (i : Size) : Set where
+  wrap : (j : Size< i) → SizeLt i
 
-d : ∀ i → D i
+loop : (d : ∀ i → SizeLt i) → ∀ i → SizeLt i → ⊥
+loop d i (wrap j) = loop d j (d j)
+
+-- -- Loops during injectivity check:
+-- loop : ∀ i → SizeLt i → ⊥
+-- loop i (wrap j) = loop j (wrap (pred j))
+
+d : ∀ i → SizeLt i
 d i = wrap (pred i)
 
 absurd : ⊥
-absurd = FIXME loop ∞ (d ∞)
+absurd = loop d ∞ (d ∞)
+
+_ = FIXME
 
 -- Testcase temporarily mutilated, original error:
--- -Issue1428a.agda:9,20-31
+--
+-- -Issue1428a.agda:..
 -- -Functions may not return sizes, thus, function type
 -- -(i : Size) → Size< i is illegal
 -- -when checking that the expression ∀ i → Size< i is a type
--- +Issue1428a.agda:22,10-15
+--
+-- +Issue1428a.agda:...
 -- +Not in scope:
--- +  FIXME at Issue1428a.agda:22,10-15
+-- +  FIXME at Issue1428a.agda:...
 -- +when scope checking FIXME

test/Fail/Issue1428a.err

@@ -1,4 +1,4 @@
-Issue1428a.agda:22,10-15
+Issue1428a.agda:29,5-10
 Not in scope:
-  FIXME at Issue1428a.agda:22,10-15
+  FIXME at Issue1428a.agda:29,5-10
 when scope checking FIXME

test/Fail/Issue1428c.agda

@@ -1,31 +1,34 @@
 -- Andreas, 2015-03-17
+-- Andreas, 2020-10-26 conform to Issue1428a
 
-open import Common.Size
+open import Agda.Builtin.Size
 
 data ⊥ : Set where
 
-data D (i : Size) : Set where
-  c : Size< i → D i
+data SizeLt (i : Size) : Set where
+  wrap : Size< i → SizeLt i
 
 -- This definition of size predecessor should be forbidden...
 module _ (i : Size) where
   postulate
     pred : Size< i
 
 -- ...otherwise the injectivity test loops here.
-iter : ∀ i → D i → ⊥
-iter i (c j) = iter j (c (pred j))
+iter : ∀ i → SizeLt i → ⊥
+iter i (wrap j) = iter j (wrap (pred j))
 
 loop : Size → ⊥
-loop i = iter i (c (pred i))
+loop i = iter i (wrap (pred i))
 
 absurd : ⊥
 absurd = FIXME loop ∞
 
--- Testcase temporarily mutilated, original error
--- -Issue1428c.agda:13,5-19
+-- Testcase temporarily mutilated, original error:
+--
+-- -Issue1428c.agda:...
 -- -We don't like postulated sizes in parametrized modules.
--- +Issue1428c.agda:23,10-15
+--
+-- +Issue1428c.agda:...
 -- +Not in scope:
--- +  FIXME at Issue1428c.agda:23,10-15
+-- +  FIXME at Issue1428c.agda:...
 -- +when scope checking FIXME

test/Fail/Issue1428c.err

@@ -1,4 +1,5 @@
-Issue1428c.agda:23,10-15
+Issue1428c.agda:24,10-15
 Not in scope:
-  FIXME at Issue1428c.agda:23,10-15
+  FIXME
+  at Issue1428c.agda:24,10-15
 when scope checking FIXME

test/Succeed/Issue1292b.agda

@@ -4,7 +4,7 @@
 
 -- {-# OPTIONS -v tc.size:20  #-}
 
-open import Common.Size
+open import Agda.Builtin.Size
 
 data Nat : {size : Size} -> Set where
   zero : {size : Size} -> Nat {↑ size}
@@ -22,3 +22,5 @@ div' zero    n = zero
 div' (suc m) n = suc (div' (sub m n) n)
 
 -- should termination check even --without-K
+
+-- -}