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
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing how the Binary tree module can be used
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module README.Data.Tree.Binary where
open import Data.List.Base
open import Data.String.Base using (String; unlines)
open import Data.Tree.Binary using (Tree; leaf; node)
open import Function.Base
open import Agda.Builtin.Equality
------------------------------------------------------------------------
-- Pretty-printing
open import Data.Tree.Binary.Show using (display)
_ : unlines (display
$ node (node (leaf [ "plum" ])
("apricot" ∷ "prune" ∷ [])
(node (leaf [ "orange" ])
("peach" ∷ [])
(node (leaf [ "kiwi" ])
("apple" ∷ "pear" ∷ [])
(leaf [ "pineapple" ]))))
("cherry" ∷ "lemon" ∷ "banana" ∷ [])
(leaf [ "yuzu" ]))
≡ "cherry
\ \lemon
\ \banana
\ \ ├ apricot
\ \ │ prune
\ \ │ ├ plum
\ \ │ └ peach
\ \ │ ├ orange
\ \ │ └ apple
\ \ │ pear
\ \ │ ├ kiwi
\ \ │ └ pineapple
\ \ └ yuzu"
_ = refl
|
