Idris2/tests/idris2/literate006/expected

1/1: Building Door (Door.lidr)
Main> >               (val # y) => ?now_4
Main> >               (True # d) => ?now_4
>               (False # d) => ?now_5
Main>  0 m : Type -> Type
 1 d : Door Open
   x : Integer
 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
-------------------------------------
now_2 : Use Many m ()
Main>  0 m : Type -> Type
 1 d : Door Closed
   x : Integer
 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
-------------------------------------
now_3 : Use Many m ()
Main> Bye for now!
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`1/1: Building Door (Door.lidr)`
Add linear pair/dependent pair to the prelude I'm playing with some linear structures and finding these useful a lot, so good to have a consistent syntax for it. '#' is chosen because it's short, looks a bit like a cross if you look at it from the right angle (!) and so as not to clash with '@@' in preorder reasoning syntax. 2020-06-12 13:18:12 +03:00			`Main> > (val # y) => ?now_4`
			`Main> > (True # d) => ?now_4`
			`> (False # d) => ?now_5`
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`Main> 0 m : Type -> Type`
			`1 d : Door Open`
			`x : Integer`
			`0 r : Res Bool (\r => (Door (if r then Open else Closed)))`
			`-------------------------------------`
			`now_2 : Use Many m ()`
			`Main> 0 m : Type -> Type`
			`1 d : Door Closed`
			`x : Integer`
			`0 r : Res Bool (\r => (Door (if r then Open else Closed)))`
			`-------------------------------------`
			`now_3 : Use Many m ()`
			`Main> Bye for now!`