aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/documentation/lux/meta/type/quotient.lux
blob: 58f9edfd5baba3dcb87051c9f23e65810babd75b (plain)
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
(.require
 [library
  [lux (.except)
   ["$" documentation]
   [data
    ["[0]" text (.only \n)
     ["%" \\format (.only format)]]]]]
 [\\library
  ["[0]" /]])

(.def .public documentation
  (.List $.Module)
  ($.module /._
            ""
            [($.definition /.class)
             ($.definition /.value)
             ($.definition /.label)
             ($.definition /.equivalence)

             ($.definition (/.Class value label)
               "The class knows how to classify/label values that are meant to be equivalent to one another.")

             ($.definition (/.Quotient value label)
               (format "A quotient value has been labeled with a class."
                       \n "All equivalent values will belong to the same class."
                       \n "This means all equivalent values possess the same label."))

             ($.definition /.quotient
               ""
               [(quotient class value)])

             ($.definition /.type
               "The Quotient type associated with a Class type."
               [(def even
                  (class even?))

                (def Even
                  Type
                  (type even))

                (is Even
                    (quotient even 123))])]
            []))