Idris2/tests/idris2/linear009/expected

1/1: Building qtt (qtt.idr)
Main>  0 m : Nat
 0 a : Type
   x : a
 0 y : a
 0 ws : Vect k a
 1 zs : Vect (S k) a
   ys : Vect m a
 0 n : Nat
------------------------------
foo : Vect (S (S (plus k m))) a
Main>  0 m : Nat
 0 a : Type
   ys : Vect m a
   x : a
 1 zs : Vect k a
 0 xs : Vect (S k) a
 0 n : Nat
------------------------------
bar : Vect (S (plus k m)) a
Main>  0 m : Nat
 0 a : Type
   ys : Vect m a
   x : a
 0 zs : Vect k a
 0 xs : Vect (S k) a
 0 n : Nat
 1 ts : Vect k a
------------------------------
baz : Vect (S (plus k m)) a
Main> Bye for now!
Allow _ for names in pi binders This is mostly to make it easier to write linear function types without having to invent names for everything, which might be noisy. Also it improves the display of linear function types when the name isn't used in the scope. 2020-05-25 15:14:51 +03:00			`1/1: Building qtt (qtt.idr)`
			`Main> 0 m : Nat`
			`0 a : Type`
			`x : a`
			`0 y : a`
			`0 ws : Vect k a`
			`1 zs : Vect (S k) a`
			`ys : Vect m a`
			`0 n : Nat`
Prettyprinting hole context 2020-08-18 15:36:34 +03:00			`------------------------------`
Allow _ for names in pi binders This is mostly to make it easier to write linear function types without having to invent names for everything, which might be noisy. Also it improves the display of linear function types when the name isn't used in the scope. 2020-05-25 15:14:51 +03:00			`foo : Vect (S (S (plus k m))) a`
			`Main> 0 m : Nat`
			`0 a : Type`
			`ys : Vect m a`
			`x : a`
			`1 zs : Vect k a`
			`0 xs : Vect (S k) a`
			`0 n : Nat`
Prettyprinting hole context 2020-08-18 15:36:34 +03:00			`------------------------------`
Allow _ for names in pi binders This is mostly to make it easier to write linear function types without having to invent names for everything, which might be noisy. Also it improves the display of linear function types when the name isn't used in the scope. 2020-05-25 15:14:51 +03:00			`bar : Vect (S (plus k m)) a`
			`Main> 0 m : Nat`
			`0 a : Type`
			`ys : Vect m a`
			`x : a`
			`0 zs : Vect k a`
			`0 xs : Vect (S k) a`
			`0 n : Nat`
			`1 ts : Vect k a`
Prettyprinting hole context 2020-08-18 15:36:34 +03:00			`------------------------------`
Allow _ for names in pi binders This is mostly to make it easier to write linear function types without having to invent names for everything, which might be noisy. Also it improves the display of linear function types when the name isn't used in the scope. 2020-05-25 15:14:51 +03:00			`baz : Vect (S (plus k m)) a`
			`Main> Bye for now!`