1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing how the Rose tree module can be used
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module README.Data.Tree.Rose where
open import Data.List.Base
open import Data.String.Base using (String; unlines)
open import Data.Tree.Rose using (Rose; node)
open import Function.Base
open import Agda.Builtin.Equality
------------------------------------------------------------------------
-- Pretty-printing
open import Data.Tree.Rose.Show using (display)
_ : unlines (display
$ node [ "one" ]
(node [ "two" ] []
∷ node ("three" ∷ "and" ∷ "four" ∷ [])
(node [ "five" ] []
∷ node [ "six" ] (node [ "seven" ] [] ∷ [])
∷ node [ "eight" ] []
∷ [])
∷ node [ "nine" ]
(node [ "ten" ] []
∷ node [ "eleven" ] [] ∷ [])
∷ []))
≡ "one
\ \ ├ two
\ \ ├ three
\ \ │ and
\ \ │ four
\ \ │ ├ five
\ \ │ ├ six
\ \ │ │ └ seven
\ \ │ └ eight
\ \ └ nine
\ \ ├ ten
\ \ └ eleven"
_ = refl
|
