poi 0.18.0

A pragmatic point-free theorem prover assistant
Documentation 
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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

_seps: "[]()\\;:,.·⨯-→{}<>=!+-*/%^&|"

31 head_tail_list = ["[" .w? .._seps!:"head" .w? "," .w? .._seps!:"tail" ".." .w? "]"]
30 head_tail_tup = ["(" .w? .._seps!:"head" .w? "," .w? .._seps!:"tail" ".." .w? ")"]
29 compute = ["compute::" .._seps!:"fun" "(" .w?
              .s!([.w? "," .w?] .._seps!:"arg") .w? ")"]
28 arity = [.._seps!:"fun" ":[arity]" .$:"arg"]
27 seq_left = {
  arity:"arity"
  no_constr:"no_constr"
  var
  val
}
26 no_constr = [.._seps!:"fun" ":!{}"]
23 knowledge = [top_expr:"left" {"<=>>":"eqveval" "<=>":"eqv"
                "=>":"red" ":=":"def"} top_expr:"right"]
22 top_expr = {
  [.w? raw_expr .w?]
  [.w? expr .w?]
}
21 alg3 = .s!([.w? "^":"^" .w?] [?[{"-":"neg"
              ["!":"not" !["\\" !"true" !"false"]] "¬":"not"}
              !.w! !.$] expr:"alg_item"])
20 alg2 = .s!([.w? {"*":"*" "/":"/" "%":"%" "&":"&" "∧":"&"} .w?] alg3:"alg")
19 alg1 = .s!([.w? {"++":"++" "+":"+" "-":"-" "|":"|" "∨":"|"} .w?] alg2:"alg")
18 alg = ["(" .w? alg_inner .w? ")"]
17 alg_inner = .s!([.w? {"<=":"<=" "<":"<" "==":"=" "=":"=" ">=":">="
          ">":">"} .w!] alg1:"alg")
16 rapp = ["(" .w? {
  ":":"rty"
  "<=":"rle"
  "<":"rlt"
  "=":"eq"
  ">=":"rge"
  ">":"rgt"
  "*":"mul"
  "/":"rdiv"
  "+":"add"
  "-":"rsub"
  "^":"rpow"
} .w! {raw_expr:"arg" expr:"arg"} .w? ")"]
15 list = ["[" .w? .s?([.w? "," .w?] {raw_expr:"item" expr:"item"}) .w? "]"]
14 tup_items_expr = tup_items:"tup"
13 tup_items = [.s!([.w? "," .w?] {raw_expr:"item" expr:"item"})]
12 tup_path_expr = tup_path:"tup"
11 tup_path = [.s!([.w? {"x" "⨯"} .w?] expr:"item") .w? {"->" "→"} .w? expr:"item"]
10 val = {
  [.._seps!:"poi" ".poi"]
  [?"\\" {
    ["true":"bool" !.$]
    ["false":!"bool" !.$]
    [.$_:"num_pi" .w? {"pi" "π"}]
    [.$_:"num_tau" .w? {"tau" "τ"}]
    [.$_:"num_eps" {[.w! "eps"] [.w? "ε"]}]
    [.$_:"num_imag3" {[.w? "imag3"] [.w? "𝐢₃"]}]
    [.$_:"num_imag2" {[.w? "imag2"] [.w? "𝐢₂"]}]
    [.$_:"num_imag" {[.w? "imag"] [.w? "𝐢"]}]
    .$_:"num"
  }]
  ["\\[" .._seps!:"singleton" "]"]
  ["[" .._seps!:"list_var" "..]"]
  ["!\\" .._seps!:"not_ret_var"]
  ["\\" .._seps!:"ret_int_var" ":int"]
  ["\\" .._seps!:"ret_pos_var" ":(>= 0)"]
  ["\\" .._seps!:"ret_neg_var" ":(< 0)"]
  ["\\" .._seps!:"ret_var"]
}
9 var = [!.$ .._seps!:"var" ?[.w? ":" .w? "\\":"ret_ty"]]
8 path_right = [.w? "[" .w? {tup_path_expr expr} .w? "]"]
7 app_right = [.w? "(" .w? {tup_items_expr expr} .w? ")"]
6 comp_right = [.w? {"." "·"} .w! expr]
5 typ_right = [.w? ":" .w? {"\\":"ret_ty" expr}]
4 constr_right = [.w? "{" .w? {tup_items_expr expr} .w? "}"]
3 seq = [{
  rapp:"rapp"
  ["(" .w? tup_items_expr:"left" .w? ")"]
  alg:"alg"
  list:"list"
  seq_left:"left"
} .r!({
  path_right:"path"
  app_right:"app"
  constr_right:"constr"
  comp_right:"comp"
  typ_right:"typ"
})]
2 expr = {
  seq:"seq"
  rapp:"rapp"
  head_tail_tup:"head_tail_tup"
  head_tail_list:"head_tail_list"
  ["(" .w? tup_items_expr .w? ")"]
  alg:"alg"
  list:"list"
  compute:"compute"
  arity:"arity"
  no_constr:"no_constr"
  val
  var
}
1 raw_expr = alg_inner:"alg"
0 doc = {
  ["#" .l([.l([!"```poi" ..."\n"?]) "```poi" .w? .s!.([.w? ";" .w?] knowledge:"knowledge") .w? "```"])]
  top_expr:"expr"
}