add missing ends of here-docs to cram tests

Author: mikeshulman

test/black/axiomK.t

@@ -4,6 +4,7 @@ Using the Martin-Löf "Jdentity type" as an indexed datatype, we can try to prov
   > def Jd (A:Type) (a:A) : A → Type ≔ data [
   > | rfl. : Jd A a a
   > ]
+  > EOF
 
   $ narya -source-only jd.ny -v -e 'def USIP (A:Type) (a:A) (e:Jd A a a) : Jd (Jd A a a) e rfl. := match e [ rfl. |-> rfl. ]'
    ￫ info[I0000]
@@ -67,6 +68,7 @@ The following indexed datatype appears in Agda bug #1025.
   > axiom A : Type
   > axiom a : A
   > def Foo : Jd A a a → Type ≔ data [ foo. : Foo rfl. ]
+  > EOF
 
   $ narya -source-only jd.ny foo.ny -v -e 'def test (e : Jd A a a) (f : Foo e) (i : Jd (Foo e) f f) : Jd (Jd (Foo e) f f) i rfl. ≔ match f [ foo. ↦ match i [ rfl. ↦ rfl. ]]'
    ￫ info[I0000]
@@ -105,6 +107,7 @@ The heterogeneous Jdentity type also figures in some inconsistencies, such as Ag
   > def Bool : Type ≔ data [ true. | false. ]
   > def D : Bool → Type ≔ data [ x. : D true. | y. : D false. ]
   > def ∅ : Type ≔ data []
+  > EOF
 
   $ narya -source-only hjd.ny -v -e 'def notpdf (u : D false.) (e : Hd (D false.) u (D true.) x.) : ∅ ≔ match e [ ]'
    ￫ info[I0000]

test/black/binop.t

@@ -19,7 +19,7 @@
   > echo (m+n)*(m+n)
   > echo n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n + n
   > echo n + n * n + n * n * n + n * n * n * n + n + n * n * n * n * n * n * n + n * n + n * n * n + n * n * n * n + n + n * n * n * n * n * n * n
-
+  > EOF
 
   $ narya -v nat.ny
    ￫ info[I0000]

test/black/compile.t

@@ -75,6 +75,7 @@ Requiring a file multiple times
   > import "two"
   > import "three"
   > axiom a2 : Id A a0 a1
+  > EOF
 
   $ narya -v four.ny
    ￫ info[I0004]

test/black/discreteness.t

@@ -124,6 +124,7 @@ Datatypes with nondiscrete parameters are not discrete:
   > axiom A : Type
   > axiom l : List A
   > def T ≔ (List A)⁽ᵈ⁾ l
+  > EOF
 
   $ narya -source-only -v -arity 1 -direction d -discreteness param.ny jd.ny -e 'def test (t1 : T) (t2 : T) : Jd T t1 t2 ≔ rfl.'
    ￫ info[I0000]
@@ -159,6 +160,7 @@ Even trivial parameters:
   > axiom A : Type
   > axiom l : param_empty A
   > def T ≔ (param_empty A)⁽ᵈ⁾ l
+  > EOF
 
   $ narya -source-only -v -arity 1 -direction d -discreteness param2.ny jd.ny -e 'def test (t1 : T) (t2 : T) : Jd T t1 t2 ≔ rfl.'
    ￫ info[I0000]
@@ -195,6 +197,7 @@ But datatypes with discrete parameters are discrete:
   > def param_empty (n:ℕ) : Type ≔ data [ ]
   > axiom l : param_empty zero.
   > def T ≔ (param_empty zero.)⁽ᵈ⁾ l
+  > EOF
 
   $ narya -source-only -v -arity 1 -direction d -discreteness param3.ny jd.ny -e 'def test (t1 : T) (t2 : T) : Jd T t1 t2 ≔ rfl.'
    ￫ info[I0000]
@@ -225,6 +228,7 @@ Datatypes with discrete indices are discrete:
   > axiom n : ℕ
   > axiom z : iszero n
   > def T ≔ (iszero n)⁽ᵈ⁾ z
+  > EOF
 
   $ narya -source-only -v -arity 1 -direction d -discreteness index.ny jd.ny -e 'def test (t1 : T) (t2 : T) : Jd T t1 t2 ≔ rfl.'
    ￫ info[I0000]
@@ -257,6 +261,7 @@ But datatypes with nondiscrete indices, even trivial ones, are not discrete:
   > def index_unit : N → Type ≔ data [ foo. : index_unit n ]
   > axiom z : index_unit n
   > def T ≔ (index_unit n)⁽ᵈ⁾ z
+  > EOF
 
   $ narya -source-only -v -arity 1 -direction d -discreteness index2.ny jd.ny -e 'def test (t1 : T) (t2 : T) : Jd T t1 t2 ≔ rfl.'
    ￫ info[I0001]
@@ -295,6 +300,7 @@ Datatypes with constructors having non-discrete arguments are not discrete:
   > def foo : Type ≔ data [ foo. (_:Type) ]
   > axiom f : foo
   > def T ≔ foo⁽ᵈ⁾ f
+  > EOF
 
   $ narya -source-only -v -arity 1 -direction d -discreteness constr.ny jd.ny -e 'def test (t1 : T) (t2 : T) : Jd T t1 t2 ≔ rfl.'
    ￫ info[I0000]

test/black/hdpi.t

@@ -8,6 +8,7 @@ Printing higher-dimensional pi-types
   > axiom B' : B → Type
   > axiom E' : refl ((X ↦ X → Type) : Type → Type) A B E A' B'
   > echo refl ((A B ↦ (x:A) → B x) : (X:Type) → (X → Type) → Type) A B E A' B' E'
+  > EOF
 
   $ narya hdpi.ny
   refl Π A B E (x ↦ A' x) (x ↦ B' x) (x ⤇ E' x.0 x.1 x.2)

test/black/import.t

@@ -89,6 +89,7 @@ Requiring a file multiple times
   > import "two"
   > import "three"
   > axiom a2 : Id A a0 a1
+  > EOF
 
   $ narya -source-only -v twothree.ny
    ￫ info[I0003]
@@ -130,6 +131,7 @@ Requiring a file multiple times
   > import "two"
   > import "three"
   > axiom a2 : Id A a0 a1
+  > EOF
 
   $ narya -source-only -v four.ny
    ￫ info[I0003]

test/black/letin.t

@@ -342,6 +342,7 @@ Let doesn't make a case tree unless it needs to:
   > echo foo
   > def foo' : prod (Type -> Type) Type := let z : prod (Type -> Type) Type := ( fst := X |-> X, snd := Type ) in z
   > echo foo'
+  > EOF
 
   $ narya -v letnocase.ny
    ￫ info[I0000]
@@ -397,6 +398,7 @@ Pattern-matching lambdas can be used in arbitrary places:
   > echo squaredec 1
   > axiom n : ℕ
   > echo squaredec n
+  > EOF
    ￫ info[I0000]
    ￮ constant ℕ defined
 
@@ -423,6 +425,7 @@ Pattern-matching lambdas can be used in arbitrary places:
   _match.0{…}
     : ℕ
 
+
 Matches in definitions of datatypes
 
   $ narya -v - <<EOF
@@ -444,6 +447,7 @@ Matches in definitions of datatypes
    ￫ info[I0000]
    ￮ constant f defined
 
+
 Matches in non-toplevel definitions of datatype
 
   $ narya -v - <<EOF
@@ -474,3 +478,4 @@ Matches in non-toplevel definitions of datatype
    ￫ info[I0000]
    ￮ constant f defined
 
+

test/black/transparent.t

@@ -30,6 +30,7 @@ Transparency and translucency
   > echo x3b
   > def y3b : prod3b ≔ (a,b)
   > echo y3b
+  > EOF
   x1
     : prod1
 
@@ -60,3 +61,4 @@ Transparency and translucency
   (a, b)
     : prod3b
 
+

test/parser/cube_variables.t

@@ -20,7 +20,8 @@ Testing parsing and printing of cube variables
   > axiom a0:A
   > axiom a1:A
   > axiom a2:Id A a0 a1
-  > echo refl f a0 a1 a2  
+  > echo refl f a0 a1 a2
+  > EOF
 
   $ narya cube_vars.ny
   x0 x1 x2 ↦ refl b