val compile_ast :
+ Compile.program ->
+ Ast.query ->
+ (State.t -> State.t) ->
+ unit Compile.queryval compile :
Compile.program ->
(depth:int ->
State.t ->
diff --git a/playground.html b/playground.html
index 5be67c932..36dfd745c 100644
--- a/playground.html
+++ b/playground.html
@@ -203,9 +203,9 @@ Regexp MatchingParsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.099
+Typechecking time: 0.065
Success:
@@ -245,11 +245,11 @@ Test Bed
5 doomed 100.
Parsing time: 0.001
+Parsing time: 0.000
Compilation time: 0.001
-Typechecking time: 0.104
+Typechecking time: 0.068
../../tests/sources/accumulate_twice2.elpi
@@ -266,11 +266,11 @@ Test Bed
Warning: constant other.doomed has no declared type.
Parsing time: 0.001
+Parsing time: 0.000
Compilation time: 0.001
-Typechecking time: 0.112
+Typechecking time: 0.070
../../tests/sources/accumulated.elpi
@@ -285,9 +285,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.104
+Typechecking time: 0.068
../../tests/sources/ackermann.elpi
@@ -326,9 +326,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.122
+Typechecking time: 0.079
Success:
@@ -363,9 +363,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.114
+Typechecking time: 0.077
Success:
@@ -395,9 +395,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.113
+Typechecking time: 0.074
Success:
@@ -498,7 +498,7 @@ Test Bed
Compilation time: 0.002
-Typechecking time: 0.120
+Typechecking time: 0.078
Success:
@@ -542,9 +542,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.106
+Typechecking time: 0.071
Success:
@@ -606,9 +606,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.120
+Typechecking time: 0.077
Success:
@@ -640,9 +640,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.064
Success:
@@ -669,9 +669,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.109
+Typechecking time: 0.071
Success:
@@ -724,9 +724,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.114
+Typechecking time: 0.078
Success:
@@ -754,9 +754,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.108
+Typechecking time: 0.073
Success:
@@ -802,9 +802,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.100
+Typechecking time: 0.065
Success:
@@ -856,9 +856,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.144
+Typechecking time: 0.098
Success:
@@ -913,9 +913,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.145
+Typechecking time: 0.093
Success:
@@ -961,9 +961,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.132
+Typechecking time: 0.088
Success:
@@ -984,9 +984,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.101
+Typechecking time: 0.065
Success:
@@ -1046,9 +1046,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.153
+Typechecking time: 0.101
Success:
@@ -1094,9 +1094,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.124
+Typechecking time: 0.083
Success:
@@ -1131,9 +1131,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.099
+Typechecking time: 0.064
Success:
@@ -1164,9 +1164,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.110
+Typechecking time: 0.073
Success:
@@ -1195,9 +1195,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.113
+Typechecking time: 0.075
Fatal error: Unification problem outside the pattern fragment. ((Data.Term.App (f, (Data.Term.Const x), [])) == (Data.Term.AppUVar (
{ Data.Term.contents = please extend this printer; uid_private = 41383 },
0,
@@ -1217,9 +1217,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.097
+Typechecking time: 0.063
Success:
@@ -1280,9 +1280,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.122
+Typechecking time: 0.079
Success:
@@ -1461,7 +1461,7 @@ Test Bed
Compilation time: 0.002
-Typechecking time: 0.148
+Typechecking time: 0.097
Type error. To ignore it, pass -no-tc.
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.100
+Typechecking time: 0.067
Success:
@@ -1579,9 +1579,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.129
+Typechecking time: 0.086
Success:
@@ -1613,9 +1613,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.120
+Typechecking time: 0.075
Success:
@@ -1645,9 +1645,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.110
+Typechecking time: 0.072
Success:
@@ -1678,9 +1678,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.114
+Typechecking time: 0.076
Success:
@@ -1719,9 +1719,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.121
+Typechecking time: 0.084
Success:
@@ -1754,9 +1754,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.112
+Typechecking time: 0.075
Success:
@@ -1782,9 +1782,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.112
+Typechecking time: 0.068
Success:
@@ -1904,7 +1904,7 @@ Test Bed
Compilation time: 0.002
-Typechecking time: 0.166
+Typechecking time: 0.110
Success:
@@ -1938,9 +1938,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.105
+Typechecking time: 0.067
Success:
@@ -1967,9 +1967,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.064
Success:
@@ -2001,9 +2001,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.115
+Typechecking time: 0.074
Success:
@@ -6098,9 +6098,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.065
Success:
@@ -6147,9 +6147,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.136
+Typechecking time: 0.089
Success:
@@ -6188,9 +6188,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.128
+Typechecking time: 0.082
Success:
@@ -6327,13 +6327,13 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.003
+Compilation time: 0.002
-Typechecking time: 0.130
+Typechecking time: 0.083
Success:
-Time: 2.244
+Time: 1.627
Constraints:
@@ -6353,9 +6353,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.102
+Typechecking time: 0.068
Success:
@@ -6403,9 +6403,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.144
+Typechecking time: 0.095
Success:
@@ -6445,9 +6445,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.131
+Typechecking time: 0.087
Success:
@@ -6553,11 +6553,11 @@ Test Bed
Compilation time: 0.002
-Typechecking time: 0.153
+Typechecking time: 0.104
Success:
-Time: 0.456
+Time: 0.293
Constraints:
@@ -6584,9 +6584,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.106
+Typechecking time: 0.068
Success:
@@ -6608,9 +6608,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.065
Success:
@@ -6884,7 +6884,7 @@ Test Bed
Compilation time: 0.002
-Typechecking time: 0.170
+Typechecking time: 0.112
Success:
@@ -6991,7 +6991,7 @@ Test Bed
Compilation time: 0.002
-Typechecking time: 0.170
+Typechecking time: 0.111
Success:
@@ -7037,18 +7037,18 @@ Test Bed
30 print Time0 "+" Time1 "+" Time2.
1.764724 + 0.074392 + 1.291222
+1.238042 + 0.052580 + 0.901364
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.101
+Typechecking time: 0.067
Success:
-Time: 3.399
+Time: 2.410
Constraints:
@@ -7111,18 +7111,18 @@ Test Bed
51 print Time0 "+" Time1 "+" Time2.
-9.239397 + 3.986891 + 0.393223
+5.671147 + 2.648835 + 0.343164
Parsing time: 0.000
Compilation time: 0.002
-Typechecking time: 0.115
+Typechecking time: 0.068
Success:
-Time: 13.630
+Time: 8.670
Constraints:
@@ -7180,18 +7180,18 @@ Test Bed
46 print Time0 "+" Time1 "+" Time2.
-8.051916 + 3.629777 + 0.270915
+5.169061 + 2.472819 + 0.205217
Parsing time: 0.000
Compilation time: 0.002
-Typechecking time: 0.101
+Typechecking time: 0.067
Success:
-Time: 11.962
+Time: 7.853
Constraints:
@@ -7216,9 +7216,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.065
Type error. To ignore it, pass -no-tc.
@@ -7270,9 +7270,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.103
+Typechecking time: 0.067
Success:
@@ -7303,9 +7303,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.112
+Typechecking time: 0.071
Success:
@@ -7339,9 +7339,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.114
+Typechecking time: 0.076
Success:
@@ -7373,9 +7373,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.121
+Typechecking time: 0.082
Success:
@@ -7434,9 +7434,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.139
+Typechecking time: 0.093
Success:
@@ -7455,9 +7455,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.096
+Typechecking time: 0.064
Success:
@@ -7530,9 +7530,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.149
+Typechecking time: 0.101
Success:
@@ -7664,9 +7664,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.124
+Typechecking time: 0.082
Success:
@@ -7696,9 +7696,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.114
+Typechecking time: 0.075
Success:
@@ -7738,9 +7738,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.129
+Typechecking time: 0.085
Success:
@@ -7772,9 +7772,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.108
+Typechecking time: 0.070
Success:
@@ -7819,9 +7819,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.136
+Typechecking time: 0.089
Success:
@@ -7954,9 +7954,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.003
+Compilation time: 0.002
-Typechecking time: 0.151
+Typechecking time: 0.102
Success:
@@ -8181,9 +8181,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.003
+Compilation time: 0.002
-Typechecking time: 0.177
+Typechecking time: 0.118
Success:
@@ -8256,9 +8256,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.150
+Typechecking time: 0.105
Type error. To ignore it, pass -no-tc.
@@ -8388,13 +8388,13 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.003
+Compilation time: 0.002
-Typechecking time: 0.162
+Typechecking time: 0.110
Success:
-Time: 2.494
+Time: 1.586
Constraints:
@@ -8416,13 +8416,13 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.096
+Typechecking time: 0.064
Success:
-Time: 0.019
+Time: 0.013
Constraints:
@@ -8440,14 +8440,14 @@ Test Bed
6 R < 10.
-1
+7
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.064
Success:
@@ -8519,11 +8519,11 @@ Test Bed
Compilation time: 0.002
-Typechecking time: 0.137
+Typechecking time: 0.092
Success:
-Time: 0.386
+Time: 0.247
Constraints:
@@ -8590,13 +8590,13 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.137
+Typechecking time: 0.090
Success:
-Time: 1.512
+Time: 1.508
Constraints:
@@ -8617,9 +8617,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.099
+Typechecking time: 0.065
../../tests/sources/restriction3.elpi
@@ -8664,9 +8664,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.103
+Typechecking time: 0.070
Success:
@@ -8696,9 +8696,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.102
+Typechecking time: 0.069
Success:
@@ -8723,9 +8723,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.064
Success:
@@ -8755,9 +8755,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.102
+Typechecking time: 0.067
Success:
@@ -8866,13 +8866,13 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.160
+Typechecking time: 0.105
Success:
-Time: 0.198
+Time: 0.131
Constraints:
@@ -8938,13 +8938,13 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.158
+Typechecking time: 0.105
Success:
-Time: 0.188
+Time: 0.128
Constraints:
@@ -8966,9 +8966,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.104
+Typechecking time: 0.068
Success:
@@ -9000,9 +9000,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.113
+Typechecking time: 0.074
Success:
@@ -9049,18 +9049,18 @@ Test Bed
31 print Time0 "+" Time1 "+" Time2.
-1.456860 + 0.067482 + 1.027066
+1.042109 + 0.049706 + 0.765615
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.099
+Typechecking time: 0.066
Success:
-Time: 2.658
+Time: 1.947
Constraints:
@@ -9120,9 +9120,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.131
+Typechecking time: 0.087
Success:
@@ -9152,11 +9152,11 @@ Test Bed
Warning: constant a.foo has no declared type.
-Parsing time: 0.001
+Parsing time: 0.000
Compilation time: 0.001
-Typechecking time: 0.118
+Typechecking time: 0.078
Success:
@@ -9183,9 +9183,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.103
+Typechecking time: 0.068
../../tests/sources/shorten_aux2.elpi
@@ -9201,9 +9201,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.108
+Typechecking time: 0.072
../../tests/sources/shorten_builtin.elpi
@@ -9219,9 +9219,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.097
+Typechecking time: 0.064
Success:
@@ -9260,9 +9260,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.117
+Typechecking time: 0.077
Success:
@@ -9297,9 +9297,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.100
+Typechecking time: 0.064
Success:
@@ -9334,9 +9334,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.099
+Typechecking time: 0.065
Success:
@@ -9360,9 +9360,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.097
+Typechecking time: 0.064
Success:
@@ -9395,9 +9395,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.110
+Typechecking time: 0.072
Success:
@@ -9420,9 +9420,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.064
Success:
@@ -9463,9 +9463,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.065
Success:
@@ -9495,9 +9495,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.103
+Typechecking time: 0.064
Success:
@@ -9527,9 +9527,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.104
+Typechecking time: 0.069
Success:
@@ -9575,9 +9575,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.135
+Typechecking time: 0.089
Success:
@@ -9606,9 +9606,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.097
+Typechecking time: 0.064
Success:
@@ -9632,9 +9632,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.096
+Typechecking time: 0.064
Success:
@@ -9671,9 +9671,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.111
+Typechecking time: 0.064
Type error. To ignore it, pass -no-tc.
@@ -9693,9 +9693,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.097
+Typechecking time: 0.065
Type error. To ignore it, pass -no-tc.
@@ -9715,9 +9715,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.064
Type error. To ignore it, pass -no-tc.
@@ -9749,9 +9749,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.065
Success:
@@ -9777,9 +9777,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.003
+Compilation time: 0.001
-Typechecking time: 0.097
+Typechecking time: 0.064
Success:
@@ -9804,7 +9804,7 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
Fatal error: exception Elpi__Compiler.CompileError(_, "looping while unfolding type abbreviation for x")
@@ -9837,9 +9837,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.098
+Typechecking time: 0.064
Success:
@@ -9868,9 +9868,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.095
+Typechecking time: 0.064
Success:
@@ -9898,9 +9898,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.096
+Typechecking time: 0.064
Success:
@@ -9921,9 +9921,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.097
+Typechecking time: 0.064
Success:
@@ -9978,9 +9978,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.108
+Typechecking time: 0.074
Success:
@@ -10011,9 +10011,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.105
+Typechecking time: 0.071
Success:
@@ -10039,9 +10039,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.002
+Compilation time: 0.001
-Typechecking time: 0.097
+Typechecking time: 0.065
Success:
@@ -10234,9 +10234,9 @@ Test Bed
Parsing time: 0.000
-Compilation time: 0.003
+Compilation time: 0.002
-Typechecking time: 0.172
+Typechecking time: 0.116
Success:
diff --git a/searchindex.js b/searchindex.js
index 19614219c..94514f848 100644
--- a/searchindex.js
+++ b/searchindex.js
@@ -1 +1 @@
-Search.setIndex({"docnames": ["about", "index", "playground"], "filenames": ["about.rst", "index.rst", "playground.rst"], "titles": ["About", "Welcome to Elpi\u2019s documentation!", "Playground"], "terms": {"thi": [0, 2], "page": [0, 2], "i": [0, 2], "both": [0, 2], "an": [0, 2], "introspect": 0, "self": 0, "document": [0, 2], "stack": 0, "befor": [0, 2], "make": [0, 2], "sure": [0, 2], "have": [0, 2], "sphinx": [0, 2], "instal": [0, 2], "pip": 0, "place": 0, "To": [0, 2], "match": 0, "visual": 0, "us": [0, 2], "commun": 0, "e": [0, 2], "g": [0, 2], "http": 0, "coq": 0, "inria": 0, "fr": 0, "distrib": 0, "current": [0, 2], "refman": 0, "rtd": 0, "theme": 0, "On": [0, 2], "debian": 0, "base": [0, 2], "system": [0, 2], "one": [0, 2], "can": [0, 2], "packag": [0, 2], "manag": 0, "apt": 0, "doc": [0, 2], "python3": 0, "follow": [0, 2], "plugin": 0, "ext": 0, "intersphinx": 0, "githubpag": 0, "name": [0, 2], "www": 0, "org": 0, "en": 0, "master": 0, "usag": 0, "html": 0, "gener": [0, 2], "link": 0, "object": [0, 2], "extern": 0, "project": 0, "either": 0, "explicitli": 0, "through": 0, "role": 0, "fallback": 0, "resolut": 0, "ani": [0, 2], "other": [0, 2], "cross": 0, "refer": [0, 2], "modul": [0, 2], "which": [0, 2], "creat": [0, 2], "nojekyl": 0, "file": [0, 2], "directori": 0, "publish": 0, "github": 0, "come": 0, "its": [0, 2], "own": 0, "helper": 0, "ar": [0, 2], "meant": 0, "directli": 0, "see": [0, 2], "playground": 0, "section": 0, "inject": [0, 2], "point": 0, "instead": [0, 2], "target": 0, "sourc": [0, 2], "tree": 0, "": [0, 2], "root": 0, "makefil": 0, "Or": 0, "option": [1, 2], "legaci": 1, "parser": [1, 2], "hook": 2, "order": 2, "run": 2, "elpi": 2, "code": 2, "snippet": 2, "output": 2, "within": 2, "built": 2, "local": 2, "eval": 2, "opam": 2, "env": 2, "build": 2, "It": 2, "doesn": 2, "t": 2, "hurt": 2, "check": 2, "dune": 2, "correctli": 2, "exec": 2, "h": 2, "block": 2, "evalu": 2, "from": 2, "convention": 2, "denot": 2, "restructuredtext": 2, "type": 2, "app": 2, "term": 2, "lam": 2, "arr": 2, "ty": 2, "nat": 2, "bool": 2, "mode": 2, "o": 2, "hd": 2, "arg": 2, "tgt": 2, "src": 2, "f": 2, "pi": 2, "x": 2, "uvar": 2, "declare_constraint": 2, "len": 2, "0": 2, "_": 2, "n": 2, "m": 2, "1": 2, "constraint": 2, "rule": 2, "k": 2, "lx": 2, "ly": 2, "print": 2, "wrong": 2, "ariti": 2, "fals": 2, "gx": 2, "tx": 2, "gy": 2, "compat": 2, "ctxconstr": 2, "new": 2, "y": 2, "main": 2, "t1_": 2, "t2_": 2, "a_": 2, "b_": 2, "2": 2, "c": 2, "z": 2, "d_": 2, "The": 2, "engin": 2, "retriev": 2, "all": 2, "direct": 2, "chang": 2, "them": 2, "literalinclud": 2, "relev": 2, "contain": 2, "exampl": 2, "captur": 2, "stdout": 2, "consol": 2, "just": 2, "after": 2, "stderr": 2, "erro": 2, "In": 2, "case": 2, "assert": 2, "onli": 2, "result": 2, "should": 2, "look": 2, "pars": 2, "time": 2, "000": 2, "compil": 2, "004": 2, "home": 2, "jwintz": 2, "develop": 2, "chr": 2, "line": 2, "7": 2, "column": 2, "60": 2, "charact": 2, "133": 2, "warn": 2, "constant": 2, "ha": 2, "declar": 2, "11": 2, "8": 2, "319": 2, "did": 2, "you": 2, "mean": 2, "std": 2, "length": 2, "28": 2, "761": 2, "typecheck": 2, "154": 2, "c1": 2, "frozen": 2, "501": 2, "c0": 2, "502": 2, "494": 2, "495": 2, "496": 2, "497": 2, "c3": 2, "499": 2, "c2": 2, "498": 2, "500": 2, "x0": 2, "x1": 2, "x2": 2, "x3": 2, "x4": 2, "x5": 2, "x6": 2, "x7": 2, "507": 2, "508": 2, "509": 2, "x8": 2, "x9": 2, "514": 2, "515": 2, "x10": 2, "520": 2, "521": 2, "x11": 2, "success": 2, "001": 2, "x12": 2, "suspend": 2, "x13": 2, "x14": 2, "state": 2, "pass": 2, "valid": 2, "v": 2, "num": 2, "zero": 2, "pred": 2, "ack": 2, "m2": 2, "n2": 2, "v2": 2, "002": 2, "099": 2, "fail": 2, "messag": 2, "error": 2, "failur": 2, "accumulate_twice1": 2, "doom": 2, "int": 2, "accumul": 2, "100": 2, "104": 2, "accumulate_twice2": 2, "namespac": 2, "runner": 2, "work": 2, "4": 2, "87": 2, "112": 2, "ackermann": 2, "yield": 2, "3": 2, "13": 2, "29": 2, "noth": 2, "530": 2, "spy": 2, "split": 2, "do": 2, "set": 2, "mem": 2, "add": 2, "remov": 2, "privat": 2, "empti": 2, "merg": 2, "min": 2, "bind": 2, "bal": 2, "height": 2, "node": 2, "cardin": 2, "element": 2, "loc": 2, "string": 2, "map": 2, "gc": 2, "stat": 2, "subset": 2, "equal": 2, "diff": 2, "inter": 2, "union": 2, "find": 2, "concat": 2, "random": 2, "self_init": 2, "rex": 2, "19": 2, "676": 2, "linear": 2, "_v": 2, "discard": 2, "v_": 2, "fresh": 2, "variabl": 2, "122": 2, "asclaus": 2, "hard": 2, "p": 2, "simpl": 2, "5": 2, "36": 2, "114": 2, "beta": 2, "b": 2, "foral": 2, "fatal": 2, "w": 2, "data": 2, "fold": 2, "right": 2, "fold2": 2, "ok": 2, "forall2": 2, "filter": 2, "flatten": 2, "flip": 2, "findal": 2, "full": 2, "field": 2, "append": 2, "appendr": 2, "113": 2, "xxx": 2, "foo": 2, "miss": 2, "506": 2, "504": 2, "503": 2, "505": 2, "512": 2, "513": 2, "519": 2, "525": 2, "526": 2, "120": 2, "chrgcd": 2, "gcd": 2, "kind": 2, "group": 2, "A": 2, "solv": 2, "99": 2, "66": 2, "14": 2, "22": 2, "77": 2, "we": 2, "forc": 2, "resumpt": 2, "6": 2, "74": 2, "106": 2, "chrleq": 2, "leq": 2, "ltn": 2, "incompat": 2, "first": 2, "refl": 2, "atisym": 2, "tran": 2, "idempot": 2, "vim": 2, "ft": 2, "lprolog": 2, "238": 2, "16": 2, "chr_nokei": 2, "prop": 2, "fst": 2, "098": 2, "chr_nokey2": 2, "bar": 2, "true": 2, "109": 2, "chr_not_cliqu": 2, "appli": 2, "list": 2, "predic": 2, "keyword": 2, "chr_sem": 2, "d": 2, "debug": 2, "drop": 2, "last": 2, "conj2": 2, "test1": 2, "test2": 2, "108": 2, "ctx_load": 2, "d1": 2, "d2": 2, "d3": 2, "d11": 2, "d22": 2, "d33": 2, "cut": 2, "queri": 2, "q": 2, "answer": 2, "ko": 2, "two": 2, "three": 2, "four": 2, "quick": 2, "79": 2, "9": 2, "117": 2, "compact": 2, "trace": 2, "counter": 2, "unix": 2, "process": 2, "close": 2, "144": 2, "cut2": 2, "expect": 2, "differ": 2, "brain": 2, "damag": 2, "semant": 2, "teyju": 2, "consist": 2, "implicit": 2, "ko1": 2, "ko2": 2, "198": 2, "240": 2, "10": 2, "233": 2, "15": 2, "260": 2, "248": 2, "exist": 2, "exists2": 2, "145": 2, "cut3": 2, "57": 2, "132": 2, "cut4": 2, "101": 2, "cut5": 2, "116": 2, "125": 2, "_y": 2, "y_": 2, "153": 2, "cut6": 2, "25": 2, "75": 2, "53": 2, "40": 2, "124": 2, "deep_index": 2, "select": 2, "claus": 2, "sinc": 2, "index": 2, "level": 2, "tc": 2, "300": 2, "_foo": 2, "110": 2, "elpi_only_llam": 2, "open": 2, "unif": 2, "problem": 2, "outsid": 2, "pattern": 2, "fragment": 2, "const": 2, "appuvar": 2, "content": 2, "pleas": 2, "extend": 2, "printer": 2, "uid_priv": 2, "41383": 2, "41382": 2, "delai": 2, "command": 2, "util": 2, "delay_outside_frag": 2, "elpi_api": 2, "deprec": 2, "end_com": 2, "097": 2, "eta": 2, "tm": 2, "macro": 2, "ctx": 2, "depth": 2, "k1": 2, "k2": 2, "branch": 2, "put": 2, "some": 2, "around": 2, "adepth": 2, "bdepth": 2, "regress": 2, "135": 2, "129": 2, "get": 2, "eta_a": 2, "as_1": 2, "as_2": 2, "as_3": 2, "uvar_1": 2, "uvar_2": 2, "uvar_3": 2, "uvar_4": 2, "uvar_5": 2, "uvar_6": 2, "var": 2, "distinct_nam": 2, "unif_1": 2, "unif_2": 2, "u": 2, "bi": 2, "x01": 2, "ter": 2, "quater": 2, "becaus": 2, "flexibl": 2, "input": 2, "prune": 2, "wa": 2, "unif_zero": 2, "37": 2, "1064": 2, "unsaf": 2, "cast": 2, "unzip": 2, "59": 2, "1639": 2, "73": 2, "2170": 2, "89": 2, "2567": 2, "17": 2, "237": 2, "97": 2, "2760": 2, "x26": 2, "x27": 2, "x28": 2, "x29": 2, "23": 2, "700": 2, "_x": 2, "x_": 2, "33": 2, "1023": 2, "34": 2, "1040": 2, "_x5": 2, "x5_": 2, "_x4": 2, "x4_": 2, "_x3": 2, "x3_": 2, "_x2": 2, "x2_": 2, "_x1": 2, "x1_": 2, "_x01": 2, "x01_": 2, "_x0": 2, "x0_": 2, "148": 2, "ignor": 2, "even": 2, "odd": 2, "succ": 2, "doubl": 2, "395": 2, "_z": 2, "z_": 2, "test3": 2, "test4": 2, "same_var": 2, "super": 2, "tricki": 2, "implement": 2, "restrict": 2, "a1": 2, "when": 2, "backtrack": 2, "lost": 2, "test5": 2, "26": 2, "577": 2, "281": 2, "159": 2, "95": 2, "43": 2, "_b": 2, "_a": 2, "fragment_exit": 2, "r": 2, "rev": 2, "replac": 2, "fragment_exit2": 2, "fragment_exit3": 2, "sigma": 2, "general_cas": 2, "20": 2, "30": 2, "55": 2, "_g": 2, "g_": 2, "121": 2, "general_case2": 2, "general_case3": 2, "hc_interp": 2, "interpret": 2, "logic": 2, "horn": 2, "illustr": 2, "reduct": 2, "realiz": 2, "substitut": 2, "also": 2, "note": 2, "third": 2, "try_claus": 2, "reduc": 2, "copi": 2, "b1": 2, "b2": 2, "box": 2, "f1": 2, "f2": 2, "tru": 2, "perp": 2, "subst": 2, "backchain": 2, "why": 2, "memb": 2, "xcon": 2, "l": 2, "imp": 2, "prog": 2, "adj": 2, "path": 2, "xnil": 2, "pathfroma": 2, "61": 2, "1823": 2, "42": 2, "1152": 2, "1103": 2, "574": 2, "65": 2, "2013": 2, "27": 2, "633": 2, "21": 2, "588": 2, "396": 2, "68": 2, "2077": 2, "suppress": 2, "12": 2, "817": 2, "_t": 2, "t_": 2, "1172": 2, "50": 2, "1381": 2, "51": 2, "1445": 2, "_c": 2, "cs_": 2, "166": 2, "hdclaus": 2, "105": 2, "heap_discard": 2, "ho": 2, "except": 2, "67": 2, "115": 2, "hollight": 2, "untrust": 2, "call": 2, "kernel": 2, "next_object": 2, "next": 2, "callback_prov": 2, "proof": 2, "complet": 2, "next_tact": 2, "tactic": 2, "update_certif": 2, "certif": 2, "applic": 2, "end_of_proof": 2, "ppterm": 2, "pretti": 2, "deftac": 2, "definit": 2, "export": 2, "trust": 2, "librari": 2, "fold2_append": 2, "put_bind": 2, "prove": 2, "function": 2, "end": 2, "ones": 2, "without": 2, "therefor": 2, "re": 2, "out": 2, "outs2": 2, "bound": 2, "fn": 2, "occur": 2, "yx": 2, "ysx": 2, "yy": 2, "hol": 2, "thm": 2, "provabl": 2, "def0": 2, "typ": 2, "loop": 2, "check1": 2, "check1def": 2, "check1thm": 2, "check1axm": 2, "check1nbt": 2, "reterm": 2, "not_defin": 2, "check_hyp": 2, "temporarili": 2, "well": 2, "formed": 2, "avoid": 2, "too": 2, "much": 2, "slow": 2, "down": 2, "ultim": 2, "due": 2, "recogn": 2, "alreadi": 2, "univ": 2, "disj_union": 2, "eq": 2, "like": 2, "known": 2, "No": 2, "propag": 2, "now": 2, "sequent": 2, "seq": 2, "gamma": 2, "hack": 2, "FOR": 2, "daemon": 2, "ign": 2, "gamma2": 2, "th": 2, "thenll": 2, "tac1": 2, "tacn": 2, "deftacl": 2, "tacl": 2, "debprint": 2, "thenl": 2, "tac": 2, "xtac": 2, "xx": 2, "id": 2, "wl": 2, "gamma1": 2, "wgamma": 2, "newl": 2, "ww": 2, "debuggin": 2, "old": 2, "itac": 2, "new_certif": 2, "pg": 2, "bad": 2, "statement": 2, "defin": 2, "def": 2, "pdef": 2, "ptype": 2, "h1": 2, "h2": 2, "return": 2, "assumpt": 2, "theorem": 2, "goaltact": 2, "hyp": 2, "axiom": 2, "st": 2, "new_basic_typ": 2, "rep": 2, "ab": 2, "repab": 2, "absrep": 2, "preph": 2, "p_tactic": 2, "typdef": 2, "decl": 2, "check1decl": 2, "hypsuchthat": 2, "goal": 2, "pgoal": 2, "existence_condit": 2, "reptyp": 2, "abstyp": 2, "absreptyp": 2, "repabstyp": 2, "impl": 2, "prephtyp": 2, "what": 2, "cont": 2, "stop": 2, "print_constraint": 2, "parseterm": 2, "ppp": 2, "xa": 2, "g2": 2, "g1": 2, "s2": 2, "s1": 2, "u2": 2, "subseteq": 2, "u1": 2, "v1": 2, "plu": 2, "safe_list_map": 2, "unifi": 2, "thei": 2, "probabl": 2, "l1": 2, "l2": 2, "list_map": 2, "pptac": 2, "parsetac": 2, "ppptac": 2, "py": 2, "pgamma": 2, "ptac1": 2, "ptacn": 2, "ptac": 2, "pa": 2, "interact": 2, "non": 2, "parse_obj": 2, "psttac": 2, "sttac": 2, "parse_thm": 2, "ptyp": 2, "parse_axiom": 2, "prep": 2, "pp_tactic": 2, "parse_nbt": 2, "ptybo": 2, "tybo": 2, "parse_def": 2, "inductive_def": 2, "predf": 2, "predf_mon": 2, "pred_i": 2, "pred_e0": 2, "pred_": 2, "exp": 2, "inductive_def_pkg": 2, "pb": 2, "pst": 2, "pp": 2, "ct": 2, "contnext": 2, "welcom": 2, "extra": 2, "light": 2, "toplevel_loop": 2, "toplevel": 2, "read_cmd": 2, "enter": 2, "flush": 2, "std_out": 2, "readterm": 2, "std_in": 2, "ph": 2, "canon": 2, "canonicaltac": 2, "pcanonicaltac": 2, "next_tactic0": 2, "list_iter_rev": 2, "print_sequ": 2, "read_in_context": 2, "cert": 2, "true_then_fals": 2, "int_tac": 2, "abort": 2, "halt": 2, "other_tac": 2, "mk_script": 2, "new_tac": 2, "non_interactive_tac": 2, "script": 2, "new_interactive_tac": 2, "interactive_tac": 2, "subproof": 2, "cscript": 2, "pscript": 2, "t2": 2, "new2": 2, "newt": 2, "mk_list_of_bounded_fresh": 2, "px": 2, "turn": 2, "t1": 2, "otac": 2, "mk_constant_list": 2, "parse_inductive_def_spec": 2, "pf": 2, "param": 2, "pty": 2, "pl": 2, "build_quantified_pred": 2, "bo": 2, "build_pred": 2, "process_constructor": 2, "rest": 2, "prove_monotonicity_thm": 2, "apredf": 2, "stm": 2, "monoton": 2, "inv": 2, "conv": 2, "depth_tac": 2, "dd": 2, "auto_monoton": 2, "state_fixpoint_def": 2, "fixpoint": 2, "prove_fix_intro_thm": 2, "predf_monoton": 2, "forall_i": 2, "rand_tac": 2, "rator_tac": 2, "land_tac": 2, "cutth": 2, "fixpoint_is_prefixpoint": 2, "lforal": 2, "lappli": 2, "applyth": 2, "itaut": 2, "prove_fix_elim_thm": 2, "opr": 2, "x23": 2, "fixpoint_subseteq_any_prefixpoint": 2, "x24": 2, "lapply_last": 2, "lforall_last": 2, "prove_intro_thm": 2, "introthm": 2, "mk_intro_thm": 2, "itauteq": 2, "mani": 2, "ON": 2, "monthm": 2, "fixdef": 2, "elimthm": 2, "out1": 2, "basic": 2, "mk_bounded_fresh": 2, "bang": 2, "bug": 2, "runtim": 2, "ml": 2, "uncom": 2, "doe": 2, "matter": 2, "btw": 2, "ff": 2, "constant_tacl": 2, "ptacl": 2, "all_equals_list": 2, "tac2": 2, "ptac2": 2, "orels": 2, "repeat": 2, "gettimeofdai": 2, "time_aft": 2, "spent": 2, "For": 2, "metavari": 2, "inspect": 2, "pseq": 2, "sym": 2, "eq_true_intro": 2, "tt": 2, "tt_intro": 2, "conj": 2, "andr": 2, "robu": 2, "version": 2, "below": 2, "nil": 2, "andl": 2, "forall_": 2, "mp": 2, "where": 2, "apply_last": 2, "pq": 2, "convers": 2, "al": 2, "strip_const": 2, "expand": 2, "argument": 2, "beta_expand": 2, "seem": 2, "pc": 2, "abs_tac": 2, "sub_tac": 2, "try": 2, "autom": 2, "todo": 2, "our": 2, "rid": 2, "hypothesi": 2, "left": 2, "tri": 2, "search": 2, "space": 2, "via": 2, "focus": 2, "not_": 2, "bit": 2, "long": 2, "want": 2, "produc": 2, "mayb": 2, "automat": 2, "somewher": 2, "els": 2, "exists_": 2, "or_": 2, "and_": 2, "eq_to_impl": 2, "not_i": 2, "sync": 2, "ff_elim": 2, "orr": 2, "orl": 2, "exists_i": 2, "n1": 2, "move": 2, "front": 2, "eq_reflex": 2, "induct": 2, "and_monoton": 2, "or_monoton": 2, "impl_monoton": 2, "not_monoton": 2, "forall_monoton": 2, "exists_monoton": 2, "the_librari": 2, "lstop": 2, "go": 2, "primivit": 2, "oper": 2, "axiomat": 2, "choic": 2, "over": 2, "choos": 2, "connect": 2, "quantifi": 2, "disjoint": 2, "inj1_disj_union": 2, "inj2_disj_union": 2, "case_disj_union": 2, "case_disj_union_inj1": 2, "e1": 2, "e2": 2, "case_disj_union_inj2": 2, "univers": 2, "injection_univ": 2, "ejection_univ": 2, "inject_limit_univ": 2, "eject_limit_univ": 2, "pair_univ": 2, "proj1_univ": 2, "proj2_univ": 2, "inj1_univ": 2, "inj2_univ": 2, "case_univ": 2, "ejection_injection_univ": 2, "eject_inject_limit_univ": 2, "proj1_pair_univ": 2, "p1": 2, "p2": 2, "proj2_pair_univ": 2, "case_univ_inj1": 2, "case_univ_inj2": 2, "or_commut": 2, "or_ff": 2, "or_tt": 2, "or_idempot": 2, "or_associ": 2, "and_commut": 2, "and_tt": 2, "and_ff": 2, "and_idempot": 2, "and_associ": 2, "and_or": 2, "or_and": 2, "ads_or_and": 2, "ads_and_or": 2, "not_or": 2, "not_and": 2, "not_not_not": 2, "impl_not_not": 2, "eq_to_impl_f": 2, "eq_to_impl_b": 2, "properti": 2, "inj": 2, "disj": 2, "pair_univ_inj_l": 2, "x20": 2, "x21": 2, "x22": 2, "x25": 2, "pair_univ_inj_r": 2, "injection_univ_inj": 2, "inj1_univ_inj": 2, "inj2_univ_inj": 2, "not_eq_inj1_inj2_univ": 2, "inj1_disj_union_inj": 2, "inj2_disj_union_inj": 2, "a2": 2, "knaster": 2, "tarski": 2, "j": 2, "in_subseteq": 2, "is_fixpoint": 2, "fixpoint_subseteq_any_fixpoint": 2, "prefixpoint_to_prefixpoint": 2, "fixpoint_is_fixpoint": 2, "found": 2, "recurs": 2, "rec": 2, "acc": 2, "accf": 2, "accf_monoton": 2, "acc_i0": 2, "acc_e0": 2, "acc_": 2, "lt": 2, "acc_i": 2, "well_found": 2, "rec_is_fixpoint": 2, "comment": 2, "requir": 2, "test_appli": 2, "test_apply2": 2, "test_itaut_1": 2, "test_monotone1": 2, "test_monotone2": 2, "test_monotone3": 2, "pnn": 2, "pnnf": 2, "pnnf_monoton": 2, "pnn_i": 2, "pnn_e0": 2, "pnn_e": 2, "pnn_tt": 2, "pnn_not": 2, "ad": 2, "hoc": 2, "fragil": 2, "x15": 2, "pnn_has_two_valu": 2, "elimin": 2, "principl": 2, "in_two": 2, "in_twof": 2, "in_twof_monoton": 2, "in_two_i": 2, "in_two_e0": 2, "in_two_": 2, "in_two_tt": 2, "in_two_ff": 2, "bool2": 2, "myrep2": 2, "myabs2": 2, "myrepabs2": 2, "myabsrep2": 2, "myproprep2": 2, "mytt": 2, "mynot": 2, "mytt_transf": 2, "mynot_transf": 2, "x18": 2, "mybool2_": 2, "x19": 2, "step0": 2, "mynot_mynot_mytt": 2, "step1": 2, "cartesian": 2, "product": 2, "inductive_typ": 2, "abstract": 2, "is_pair": 2, "prod": 2, "prod_rep": 2, "prod_ab": 2, "prod_repab": 2, "prod_absrep": 2, "prod_proprep": 2, "pair": 2, "snd": 2, "usual": 2, "lemma": 2, "natur": 2, "number": 2, "is_nat": 2, "is_natf": 2, "is_nat_monoton": 2, "is_nat_i": 2, "is_nat_e0": 2, "is_nat_": 2, "is_nat_z": 2, "nat_rep": 2, "nat_ab": 2, "nat_repab": 2, "nat_absrep": 2, "nat_proprep": 2, "consequ": 2, "transfer": 2, "nat_": 2, "nat_abs_inj": 2, "nat_rep_inj": 2, "s_inj": 2, "not_equal_z_": 2, "nat_cas": 2, "nat_case_z": 2, "nat_case_": 2, "pred_well_found": 2, "nat_recf": 2, "nat_rec": 2, "nat_rec_ok0": 2, "nat_rec_ok": 2, "arithmet": 2, "sum": 2, "plus_z": 2, "plus_": 2, "plus_n_z": 2, "plus_n_": 2, "plus_comm": 2, "statu": 2, "depend": 2, "converion": 2, "sometim": 2, "diverg": 2, "progress": 2, "myprop": 2, "provid": 2, "wit": 2, "remain": 2, "free": 2, "If": 2, "could": 2, "hand": 2, "would": 2, "need": 2, "symptom": 2, "more": 2, "never": 2, "wai": 2, "atm": 2, "apply_2": 2, "veri": 2, "same": 2, "must": 2, "occurr": 2, "still": 2, "fix": 2, "about": 2, "handl": 2, "discuss": 2, "enrico": 2, "he": 2, "shot": 2, "optim": 2, "possibl": 2, "IN": 2, "unimpl": 2, "onc": 2, "let": 2, "reach": 2, "becom": 2, "user": 2, "hypothes": 2, "least": 2, "But": 2, "better": 2, "bidirect": 2, "successor": 2, "predecessor": 2, "prover": 2, "lambdaprolog": 2, "interfac": 2, "There": 2, "leancop": 2, "prolog": 2, "trick": 2, "small": 2, "formal": 2, "possibli": 2, "everyth": 2, "decis": 2, "procedur": 2, "ring": 2, "inequ": 2, "231": 2, "18": 2, "8433": 2, "malform": 2, "hollight_legaci": 2, "infixr": 2, "126": 2, "arrow": 2, "infixl": 2, "255": 2, "infix": 2, "128": 2, "127": 2, "implic": 2, "iff": 2, "membership": 2, "130": 2, "24": 2, "mixfix": 2, "support": 2, "token": 2, "famili": 2, "identifi": 2, "start": 2, "belong": 2, "preced": 2, "associ": 2, "higher": 2, "than": 2, "here": 2, "tabl": 2, "repres": 2, "symbol": 2, "mark": 2, "cannot": 2, "eg": 2, "while": 2, "increas": 2, "fixiti": 2, "div": 2, "mod": 2, "prefix": 2, "postfix": 2, "stai": 2, "ask": 2, "skip": 2, "As": 2, "facil": 2, "ast": 2, "verifi": 2, "how": 2, "text": 2, "echo": 2, "myformula": 2, "hyp_uvar": 2, "shoud": 2, "31": 2, "62": 2, "136": 2, "impl2": 2, "index2": 2, "iter": 2, "999999": 2, "111": 2, "2318": 2, "003": 2, "244": 2, "io_colon": 2, "102": 2, "lambda": 2, "infer": 2, "simpli": 2, "appl": 2, "288": 2, "186": 2, "234": 2, "330": 2, "lambda2": 2, "41": 2, "131": 2, "lambda3": 2, "termifi": 2, "x16": 2, "x17": 2, "mult": 2, "ten": 2, "thousand": 2, "866": 2, "178": 2, "278": 2, "221": 2, "847": 2, "959": 2, "45": 2, "1020": 2, "456": 2, "list_as_conj": 2, "done": 2, "list_comma": 2, "llam": 2, "dummi": 2, "clause1": 2, "clause2": 2, "prune_arg": 2, "prune_arg2": 2, "prune_arg3": 2, "whatev": 2, "clause3": 2, "so": 2, "alon": 2, "529": 2, "476": 2, "459": 2, "400": 2, "383": 2, "_f": 2, "f_": 2, "c4": 2, "c5": 2, "c6": 2, "170": 2, "llamchr": 2, "resili": 2, "both_or_non": 2, "watch": 2, "becasus": 2, "deal": 2, "dirti": 2, "context": 2, "b2n": 2, "216": 2, "798": 2, "710": 2, "457": 2, "893": 2, "751": 2, "_p": 2, "p_": 2, "xr": 2, "4096": 2, "cmp_term": 2, "time0": 2, "time1": 2, "pr": 2, "broken": 2, "time2": 2, "764724": 2, "074392": 2, "291222": 2, "399": 2, "map_list": 2, "assoc": 2, "239397": 2, "986891": 2, "393223": 2, "630": 2, "map_list_opt": 2, "051916": 2, "629777": 2, "270915": 2, "962": 2, "name_builtin": 2, "named_clauses00": 2, "name1": 2, "named_clauses01": 2, "unabl": 2, "graft": 2, "named_clauses02": 2, "103": 2, "namespaces00": 2, "aux": 2, "rl": 2, "174": 2, "namespaces01": 2, "toto": 2, "insid": 2, "baz": 2, "namespaces02": 2, "namespaces03": 2, "foo1": 2, "foo2": 2, "foo3": 2, "foo4": 2, "187": 2, "168": 2, "139": 2, "nil_con": 2, "con": 2, "096": 2, "notat": 2, "190": 2, "191": 2, "prefixr": 2, "postfixl": 2, "200": 2, "uu": 2, "cd": 2, "zip": 2, "151": 2, "269": 2, "_d": 2, "149": 2, "notation_error": 2, "notation_legaci": 2, "patternunif": 2, "patternunif2": 2, "32": 2, "pi3": 2, "pi5": 2, "bam": 2, "152": 2, "85": 2, "56": 2, "pnf": 2, "transform": 2, "formula": 2, "prenex": 2, "normal": 2, "form": 2, "assum": 2, "classic": 2, "equival": 2, "analyz": 2, "structur": 2, "includ": 2, "modifi": 2, "analysi": 2, "quant_fre": 2, "atom": 2, "termp": 2, "appear": 2, "head": 2, "immedi": 2, "subformula": 2, "proposit": 2, "top": 2, "OF": 2, "f3": 2, "f4": 2, "91": 2, "3225": 2, "688": 2, "475": 2, "855": 2, "891": 2, "93": 2, "3271": 2, "_f4": 2, "f4_": 2, "_f3": 2, "f3_": 2, "_f2": 2, "f2_": 2, "_f1": 2, "f1_": 2, "polymorphic_vari": 2, "langag": 2, "polymorph": 2, "variant": 2, "unari": 2, "funnam": 2, "program": 2, "fun": 2, "distinct": 2, "btl": 2, "ttl": 2, "origti": 2, "check_domain": 2, "check_codomain": 2, "bodi": 2, "is_subset": 2, "is_subset_": 2, "tl": 2, "tl1": 2, "mem_": 2, "check_term": 2, "accord": 2, "ocaml": 2, "ref": 2, "kill": 2, "hindlei": 2, "milner": 2, "interest": 2, "singleton": 2, "up": 2, "trigger": 2, "confus": 2, "between": 2, "mess": 2, "happen": 2, "is_ground": 2, "main1": 2, "Of": 2, "ig": 2, "og": 2, "special": 2, "main2": 2, "ih1": 2, "oh1": 2, "ih2": 2, "oh2": 2, "84": 2, "2748": 2, "2542": 2, "1118": 2, "1008": 2, "3786": 2, "3251": 2, "958": 2, "729": 2, "88": 2, "2860": 2, "80": 2, "2645": 2, "interspers": 2, "35": 2, "1158": 2, "81": 2, "2697": 2, "177": 2, "150": 2, "queen": 2, "less": 2, "neq": 2, "rang": 2, "queens_aux": 2, "unplacedq": 2, "safeq": 2, "unplacedqs1": 2, "not_attack": 2, "not_attack_aux": 2, "dummy1": 2, "dummy2": 2, "first_claus": 2, "no_more_ch": 2, "m1": 2, "tenthousand": 2, "189": 2, "49": 2, "1240": 2, "348": 2, "431": 2, "204": 2, "52": 2, "1389": 2, "649": 2, "_dummy2": 2, "dummy2_": 2, "_dummy1": 2, "dummy1_": 2, "54": 2, "1428": 2, "1471": 2, "1532": 2, "162": 2, "quote_syntax": 2, "builtin": 2, "019": 2, "reduce_cbn": 2, "xxxxxxxxx": 2, "cbn": 2, "y2": 2, "ONE": 2, "six": 2, "twelv": 2, "nine": 2, "five": 2, "285": 2, "211": 2, "563": 2, "_nine": 2, "nine_": 2, "_twelv": 2, "twelve_": 2, "137": 2, "386": 2, "reduce_cbv": 2, "cbv": 2, "r2": 2, "351": 2, "restriction3": 2, "nr": 2, "exit": 2, "442": 2, "restriction4": 2, "restriction5": 2, "restriction6": 2, "yap": 2, "027": 2, "771": 2, "hashtbl": 2, "528": 2, "ineffici": 2, "681": 2, "899": 2, "lvl": 2, "flat": 2, "763": 2, "629": 2, "083": 2, "068": 2, "90": 2, "48": 2, "ocamlopt": 2, "014": 2, "ocamlc": 2, "024": 2, "033": 2, "257": 2, "72": 2, "ulimit": 2, "81920": 2, "newlazi": 2, "lazi": 2, "eager": 2, "78": 2, "00": 2, "auto": 2, "39": 2, "hash": 2, "38": 2, "64": 2, "man": 2, "83": 2, "44": 2, "63": 2, "effici": 2, "ii": 2, "70": 2, "desper": 2, "desperate2": 2, "desperate3": 2, "1827": 2, "1857": 2, "47": 2, "2004": 2, "160": 2, "rev14": 2, "171": 2, "158": 2, "188": 2, "same_term": 2, "self_assign": 2, "succe": 2, "456860": 2, "067482": 2, "027066": 2, "658": 2, "shorten": 2, "shorten2": 2, "shorten_aux": 2, "shorten_aux2": 2, "118": 2, "shorten_builtin": 2, "shorten_tri": 2, "concat1": 2, "escap": 2, "_e": 2, "e_": 2, "_ab": 2, "ab_": 2, "spill_and": 2, "omit": 2, "purpos": 2, "spill_impl": 2, "spill_lam": 2, "trace2": 2, "trace_chr": 2, "trace_cut": 2, "trace_findal": 2, "trail": 2, "outcom": 2, "typeabbrv": 2, "typeabbrev": 2, "typeabbrv1": 2, "typeabbrv10": 2, "tmp": 2, "x30": 2, "x31": 2, "typeabbrv11": 2, "typeabbrv12": 2, "typeabbrv2": 2, "duplic": 2, "abbrevi": 2, "previou": 2, "typeabbrv3": 2, "typeabbrv4": 2, "typeabbrv5": 2, "elpi__compil": 2, "compileerror": 2, "unfold": 2, "typeabbrv6": 2, "unbound": 2, "typeabbrv7": 2, "typeabbrv8": 2, "095": 2, "typeabbrv9": 2, "uminu": 2, "uvar_chr": 2, "mk": 2, "meta": 2, "438": 2, "731": 2, "_x10": 2, "x10_": 2, "variadic_declare_constraint": 2, "tye": 2, "mono": 2, "size": 2, "comma": 2, "integ": 2, "fp": 2, "overbar": 2, "poli": 2, "fresh_": 2, "polyt": 2, "vt": 2, "vg": 2, "tp": 2, "xt": 2, "tq": 2, "76": 2, "1561": 2, "82": 2, "1693": 2, "2038": 2, "2025": 2, "107": 2, "2408": 2, "_tq": 2, "tq_": 2, "172": 2, "w_legaci": 2, "zebra": 2, "elp": 2, "_build": 2, "default": 2, "lib": 2}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"about": 0, "prerequisit": [0, 2], "extens": 0, "build": 0, "welcom": 1, "elpi": 1, "": 1, "document": 1, "api": 1, "playground": 2, "syntax": 2, "regexp": 2, "match": 2, "test": 2, "bed": 2}, "envversion": {"sphinx.domains.c": 3, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 9, "sphinx.domains.index": 1, "sphinx.domains.javascript": 3, "sphinx.domains.math": 2, "sphinx.domains.python": 4, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx.ext.intersphinx": 1, "sphinx": 60}, "alltitles": {"About": [[0, "about"]], "Prerequisites": [[0, "prerequisites"], [2, "prerequisites"]], "Extensions": [[0, "extensions"]], "Building": [[0, "building"]], "Welcome to Elpi\u2019s documentation!": [[1, "welcome-to-elpi-s-documentation"]], "API:": [[1, null]], "Playground": [[2, "playground"]], "Syntax": [[2, "syntax"]], "Regexp Matching": [[2, "regexp-matching"]], "Test Bed": [[2, "test-bed"]]}, "indexentries": {}})
\ No newline at end of file
+Search.setIndex({"docnames": ["about", "index", "playground"], "filenames": ["about.rst", "index.rst", "playground.rst"], "titles": ["About", "Welcome to Elpi\u2019s documentation!", "Playground"], "terms": {"thi": [0, 2], "page": [0, 2], "i": [0, 2], "both": [0, 2], "an": [0, 2], "introspect": 0, "self": 0, "document": [0, 2], "stack": 0, "befor": [0, 2], "make": [0, 2], "sure": [0, 2], "have": [0, 2], "sphinx": [0, 2], "instal": [0, 2], "pip": 0, "place": 0, "To": [0, 2], "match": 0, "visual": 0, "us": [0, 2], "commun": 0, "e": [0, 2], "g": [0, 2], "http": 0, "coq": 0, "inria": 0, "fr": 0, "distrib": 0, "current": [0, 2], "refman": 0, "rtd": 0, "theme": 0, "On": [0, 2], "debian": 0, "base": [0, 2], "system": [0, 2], "one": [0, 2], "can": [0, 2], "packag": [0, 2], "manag": 0, "apt": 0, "doc": [0, 2], "python3": 0, "follow": [0, 2], "plugin": 0, "ext": 0, "intersphinx": 0, "githubpag": 0, "name": [0, 2], "www": 0, "org": 0, "en": 0, "master": 0, "usag": 0, "html": 0, "gener": [0, 2], "link": 0, "object": [0, 2], "extern": 0, "project": 0, "either": 0, "explicitli": 0, "through": 0, "role": 0, "fallback": 0, "resolut": 0, "ani": [0, 2], "other": [0, 2], "cross": 0, "refer": [0, 2], "modul": [0, 2], "which": [0, 2], "creat": [0, 2], "nojekyl": 0, "file": [0, 2], "directori": 0, "publish": 0, "github": 0, "come": 0, "its": [0, 2], "own": 0, "helper": 0, "ar": [0, 2], "meant": 0, "directli": 0, "see": [0, 2], "playground": 0, "section": 0, "inject": [0, 2], "point": 0, "instead": [0, 2], "target": 0, "sourc": [0, 2], "tree": 0, "": [0, 2], "root": 0, "makefil": 0, "Or": 0, "option": [1, 2], "legaci": 1, "parser": [1, 2], "hook": 2, "order": 2, "run": 2, "elpi": 2, "code": 2, "snippet": 2, "output": 2, "within": 2, "built": 2, "local": 2, "eval": 2, "opam": 2, "env": 2, "build": 2, "It": 2, "doesn": 2, "t": 2, "hurt": 2, "check": 2, "dune": 2, "correctli": 2, "exec": 2, "h": 2, "block": 2, "evalu": 2, "from": 2, "convention": 2, "denot": 2, "restructuredtext": 2, "type": 2, "app": 2, "term": 2, "lam": 2, "arr": 2, "ty": 2, "nat": 2, "bool": 2, "mode": 2, "o": 2, "hd": 2, "arg": 2, "tgt": 2, "src": 2, "f": 2, "pi": 2, "x": 2, "uvar": 2, "declare_constraint": 2, "len": 2, "0": 2, "_": 2, "n": 2, "m": 2, "1": 2, "constraint": 2, "rule": 2, "k": 2, "lx": 2, "ly": 2, "print": 2, "wrong": 2, "ariti": 2, "fals": 2, "gx": 2, "tx": 2, "gy": 2, "compat": 2, "ctxconstr": 2, "new": 2, "y": 2, "main": 2, "t1_": 2, "t2_": 2, "a_": 2, "b_": 2, "2": 2, "c": 2, "z": 2, "d_": 2, "The": 2, "engin": 2, "retriev": 2, "all": 2, "direct": 2, "chang": 2, "them": 2, "literalinclud": 2, "relev": 2, "contain": 2, "exampl": 2, "captur": 2, "stdout": 2, "consol": 2, "just": 2, "after": 2, "stderr": 2, "erro": 2, "In": 2, "case": 2, "assert": 2, "onli": 2, "result": 2, "should": 2, "look": 2, "pars": 2, "time": 2, "000": 2, "compil": 2, "004": 2, "home": 2, "jwintz": 2, "develop": 2, "chr": 2, "line": 2, "7": 2, "column": 2, "60": 2, "charact": 2, "133": 2, "warn": 2, "constant": 2, "ha": 2, "declar": 2, "11": 2, "8": 2, "319": 2, "did": 2, "you": 2, "mean": 2, "std": 2, "length": 2, "28": 2, "761": 2, "typecheck": 2, "154": 2, "c1": 2, "frozen": 2, "501": 2, "c0": 2, "502": 2, "494": 2, "495": 2, "496": 2, "497": 2, "c3": 2, "499": 2, "c2": 2, "498": 2, "500": 2, "x0": 2, "x1": 2, "x2": 2, "x3": 2, "x4": 2, "x5": 2, "x6": 2, "x7": 2, "507": 2, "508": 2, "509": 2, "x8": 2, "x9": 2, "514": 2, "515": 2, "x10": 2, "520": 2, "521": 2, "x11": 2, "success": 2, "001": 2, "x12": 2, "suspend": 2, "x13": 2, "x14": 2, "state": 2, "pass": 2, "valid": 2, "v": 2, "num": 2, "zero": 2, "pred": 2, "ack": 2, "m2": 2, "n2": 2, "v2": 2, "065": 2, "fail": 2, "messag": 2, "error": 2, "failur": 2, "accumulate_twice1": 2, "doom": 2, "int": 2, "accumul": 2, "100": 2, "068": 2, "accumulate_twice2": 2, "namespac": 2, "runner": 2, "work": 2, "4": 2, "87": 2, "070": 2, "ackermann": 2, "yield": 2, "3": 2, "13": 2, "29": 2, "noth": 2, "530": 2, "spy": 2, "split": 2, "do": 2, "set": 2, "mem": 2, "add": 2, "remov": 2, "privat": 2, "empti": 2, "merg": 2, "min": 2, "bind": 2, "bal": 2, "height": 2, "node": 2, "cardin": 2, "element": 2, "loc": 2, "string": 2, "map": 2, "gc": 2, "stat": 2, "subset": 2, "equal": 2, "diff": 2, "inter": 2, "union": 2, "find": 2, "concat": 2, "random": 2, "self_init": 2, "rex": 2, "19": 2, "676": 2, "linear": 2, "_v": 2, "discard": 2, "v_": 2, "fresh": 2, "variabl": 2, "079": 2, "asclaus": 2, "hard": 2, "p": 2, "simpl": 2, "5": 2, "36": 2, "077": 2, "beta": 2, "b": 2, "foral": 2, "fatal": 2, "w": 2, "data": 2, "fold": 2, "right": 2, "fold2": 2, "ok": 2, "forall2": 2, "filter": 2, "flatten": 2, "flip": 2, "findal": 2, "full": 2, "field": 2, "append": 2, "appendr": 2, "074": 2, "xxx": 2, "foo": 2, "miss": 2, "506": 2, "504": 2, "503": 2, "505": 2, "512": 2, "513": 2, "519": 2, "525": 2, "526": 2, "002": 2, "078": 2, "chrgcd": 2, "gcd": 2, "kind": 2, "group": 2, "A": 2, "solv": 2, "99": 2, "66": 2, "14": 2, "22": 2, "77": 2, "we": 2, "forc": 2, "resumpt": 2, "6": 2, "74": 2, "071": 2, "chrleq": 2, "leq": 2, "ltn": 2, "incompat": 2, "first": 2, "refl": 2, "atisym": 2, "tran": 2, "idempot": 2, "vim": 2, "ft": 2, "lprolog": 2, "238": 2, "16": 2, "chr_nokei": 2, "prop": 2, "fst": 2, "064": 2, "chr_nokey2": 2, "bar": 2, "true": 2, "chr_not_cliqu": 2, "appli": 2, "list": 2, "predic": 2, "keyword": 2, "chr_sem": 2, "d": 2, "debug": 2, "drop": 2, "last": 2, "conj2": 2, "test1": 2, "test2": 2, "073": 2, "ctx_load": 2, "d1": 2, "d2": 2, "d3": 2, "d11": 2, "d22": 2, "d33": 2, "cut": 2, "queri": 2, "q": 2, "answer": 2, "ko": 2, "two": 2, "three": 2, "four": 2, "108": 2, "quick": 2, "79": 2, "9": 2, "117": 2, "compact": 2, "trace": 2, "counter": 2, "unix": 2, "process": 2, "close": 2, "098": 2, "cut2": 2, "expect": 2, "differ": 2, "brain": 2, "damag": 2, "semant": 2, "teyju": 2, "consist": 2, "implicit": 2, "ko1": 2, "ko2": 2, "198": 2, "240": 2, "10": 2, "233": 2, "15": 2, "260": 2, "248": 2, "exist": 2, "exists2": 2, "093": 2, "cut3": 2, "57": 2, "088": 2, "cut4": 2, "cut5": 2, "116": 2, "125": 2, "_y": 2, "y_": 2, "101": 2, "cut6": 2, "25": 2, "75": 2, "53": 2, "40": 2, "083": 2, "deep_index": 2, "select": 2, "claus": 2, "sinc": 2, "index": 2, "level": 2, "tc": 2, "300": 2, "_foo": 2, "elpi_only_llam": 2, "open": 2, "075": 2, "unif": 2, "problem": 2, "outsid": 2, "pattern": 2, "fragment": 2, "const": 2, "appuvar": 2, "content": 2, "pleas": 2, "extend": 2, "printer": 2, "uid_priv": 2, "41383": 2, "41382": 2, "delai": 2, "command": 2, "util": 2, "delay_outside_frag": 2, "elpi_api": 2, "deprec": 2, "end_com": 2, "063": 2, "eta": 2, "tm": 2, "macro": 2, "ctx": 2, "depth": 2, "k1": 2, "k2": 2, "branch": 2, "put": 2, "some": 2, "around": 2, "adepth": 2, "bdepth": 2, "regress": 2, "135": 2, "129": 2, "get": 2, "eta_a": 2, "as_1": 2, "as_2": 2, "as_3": 2, "uvar_1": 2, "uvar_2": 2, "uvar_3": 2, "uvar_4": 2, "uvar_5": 2, "uvar_6": 2, "var": 2, "distinct_nam": 2, "unif_1": 2, "unif_2": 2, "u": 2, "bi": 2, "x01": 2, "ter": 2, "quater": 2, "becaus": 2, "flexibl": 2, "input": 2, "prune": 2, "wa": 2, "unif_zero": 2, "37": 2, "1064": 2, "unsaf": 2, "cast": 2, "unzip": 2, "59": 2, "1639": 2, "73": 2, "2170": 2, "89": 2, "2567": 2, "17": 2, "237": 2, "97": 2, "2760": 2, "x26": 2, "x27": 2, "x28": 2, "x29": 2, "23": 2, "700": 2, "_x": 2, "x_": 2, "33": 2, "1023": 2, "34": 2, "1040": 2, "_x5": 2, "x5_": 2, "_x4": 2, "x4_": 2, "_x3": 2, "x3_": 2, "_x2": 2, "x2_": 2, "_x1": 2, "x1_": 2, "_x01": 2, "x01_": 2, "_x0": 2, "x0_": 2, "097": 2, "ignor": 2, "even": 2, "odd": 2, "succ": 2, "doubl": 2, "395": 2, "_z": 2, "z_": 2, "067": 2, "test3": 2, "test4": 2, "same_var": 2, "super": 2, "tricki": 2, "implement": 2, "restrict": 2, "a1": 2, "when": 2, "backtrack": 2, "lost": 2, "test5": 2, "26": 2, "577": 2, "281": 2, "159": 2, "95": 2, "43": 2, "_b": 2, "_a": 2, "086": 2, "fragment_exit": 2, "r": 2, "rev": 2, "replac": 2, "fragment_exit2": 2, "072": 2, "fragment_exit3": 2, "sigma": 2, "076": 2, "general_cas": 2, "20": 2, "30": 2, "55": 2, "_g": 2, "g_": 2, "084": 2, "general_case2": 2, "general_case3": 2, "hc_interp": 2, "interpret": 2, "logic": 2, "horn": 2, "illustr": 2, "reduct": 2, "realiz": 2, "substitut": 2, "also": 2, "note": 2, "third": 2, "try_claus": 2, "reduc": 2, "copi": 2, "b1": 2, "b2": 2, "box": 2, "f1": 2, "f2": 2, "tru": 2, "perp": 2, "subst": 2, "backchain": 2, "why": 2, "memb": 2, "xcon": 2, "l": 2, "imp": 2, "prog": 2, "adj": 2, "path": 2, "xnil": 2, "pathfroma": 2, "61": 2, "1823": 2, "42": 2, "1152": 2, "1103": 2, "574": 2, "65": 2, "2013": 2, "27": 2, "633": 2, "21": 2, "588": 2, "396": 2, "68": 2, "2077": 2, "suppress": 2, "12": 2, "817": 2, "_t": 2, "t_": 2, "1172": 2, "50": 2, "1381": 2, "51": 2, "1445": 2, "_c": 2, "cs_": 2, "110": 2, "hdclaus": 2, "heap_discard": 2, "ho": 2, "except": 2, "67": 2, "hollight": 2, "untrust": 2, "call": 2, "kernel": 2, "next_object": 2, "next": 2, "callback_prov": 2, "proof": 2, "complet": 2, "next_tact": 2, "tactic": 2, "update_certif": 2, "certif": 2, "applic": 2, "end_of_proof": 2, "ppterm": 2, "pretti": 2, "deftac": 2, "definit": 2, "export": 2, "trust": 2, "librari": 2, "fold2_append": 2, "put_bind": 2, "prove": 2, "function": 2, "end": 2, "ones": 2, "without": 2, "therefor": 2, "re": 2, "out": 2, "outs2": 2, "bound": 2, "fn": 2, "occur": 2, "yx": 2, "ysx": 2, "yy": 2, "hol": 2, "thm": 2, "provabl": 2, "def0": 2, "typ": 2, "loop": 2, "check1": 2, "check1def": 2, "check1thm": 2, "check1axm": 2, "check1nbt": 2, "reterm": 2, "not_defin": 2, "check_hyp": 2, "temporarili": 2, "well": 2, "formed": 2, "avoid": 2, "too": 2, "much": 2, "slow": 2, "down": 2, "ultim": 2, "due": 2, "recogn": 2, "alreadi": 2, "univ": 2, "disj_union": 2, "eq": 2, "like": 2, "known": 2, "No": 2, "propag": 2, "now": 2, "sequent": 2, "seq": 2, "gamma": 2, "hack": 2, "FOR": 2, "daemon": 2, "ign": 2, "gamma2": 2, "th": 2, "thenll": 2, "tac1": 2, "tacn": 2, "deftacl": 2, "tacl": 2, "debprint": 2, "thenl": 2, "tac": 2, "xtac": 2, "xx": 2, "id": 2, "wl": 2, "gamma1": 2, "wgamma": 2, "newl": 2, "ww": 2, "debuggin": 2, "old": 2, "itac": 2, "new_certif": 2, "pg": 2, "bad": 2, "statement": 2, "defin": 2, "def": 2, "pdef": 2, "ptype": 2, "h1": 2, "h2": 2, "return": 2, "assumpt": 2, "theorem": 2, "goaltact": 2, "hyp": 2, "axiom": 2, "st": 2, "new_basic_typ": 2, "rep": 2, "ab": 2, "repab": 2, "absrep": 2, "preph": 2, "p_tactic": 2, "typdef": 2, "decl": 2, "check1decl": 2, "hypsuchthat": 2, "goal": 2, "pgoal": 2, "existence_condit": 2, "reptyp": 2, "abstyp": 2, "absreptyp": 2, "repabstyp": 2, "impl": 2, "prephtyp": 2, "what": 2, "cont": 2, "stop": 2, "print_constraint": 2, "parseterm": 2, "ppp": 2, "xa": 2, "g2": 2, "g1": 2, "s2": 2, "s1": 2, "u2": 2, "subseteq": 2, "u1": 2, "v1": 2, "plu": 2, "safe_list_map": 2, "unifi": 2, "thei": 2, "probabl": 2, "l1": 2, "l2": 2, "list_map": 2, "pptac": 2, "parsetac": 2, "ppptac": 2, "py": 2, "pgamma": 2, "ptac1": 2, "ptacn": 2, "ptac": 2, "pa": 2, "interact": 2, "non": 2, "parse_obj": 2, "psttac": 2, "sttac": 2, "parse_thm": 2, "ptyp": 2, "parse_axiom": 2, "prep": 2, "pp_tactic": 2, "parse_nbt": 2, "ptybo": 2, "tybo": 2, "parse_def": 2, "inductive_def": 2, "predf": 2, "predf_mon": 2, "pred_i": 2, "pred_e0": 2, "pred_": 2, "exp": 2, "inductive_def_pkg": 2, "pb": 2, "pst": 2, "pp": 2, "ct": 2, "contnext": 2, "welcom": 2, "extra": 2, "light": 2, "toplevel_loop": 2, "toplevel": 2, "read_cmd": 2, "enter": 2, "flush": 2, "std_out": 2, "readterm": 2, "std_in": 2, "ph": 2, "canon": 2, "canonicaltac": 2, "pcanonicaltac": 2, "next_tactic0": 2, "list_iter_rev": 2, "print_sequ": 2, "read_in_context": 2, "cert": 2, "true_then_fals": 2, "int_tac": 2, "abort": 2, "halt": 2, "other_tac": 2, "mk_script": 2, "new_tac": 2, "non_interactive_tac": 2, "script": 2, "new_interactive_tac": 2, "interactive_tac": 2, "subproof": 2, "cscript": 2, "pscript": 2, "t2": 2, "new2": 2, "newt": 2, "mk_list_of_bounded_fresh": 2, "px": 2, "turn": 2, "t1": 2, "otac": 2, "mk_constant_list": 2, "parse_inductive_def_spec": 2, "pf": 2, "param": 2, "pty": 2, "pl": 2, "build_quantified_pred": 2, "bo": 2, "build_pred": 2, "process_constructor": 2, "rest": 2, "prove_monotonicity_thm": 2, "apredf": 2, "stm": 2, "monoton": 2, "inv": 2, "conv": 2, "depth_tac": 2, "dd": 2, "auto_monoton": 2, "state_fixpoint_def": 2, "fixpoint": 2, "prove_fix_intro_thm": 2, "predf_monoton": 2, "forall_i": 2, "rand_tac": 2, "rator_tac": 2, "land_tac": 2, "cutth": 2, "fixpoint_is_prefixpoint": 2, "lforal": 2, "lappli": 2, "applyth": 2, "itaut": 2, "prove_fix_elim_thm": 2, "opr": 2, "x23": 2, "fixpoint_subseteq_any_prefixpoint": 2, "x24": 2, "lapply_last": 2, "lforall_last": 2, "prove_intro_thm": 2, "introthm": 2, "mk_intro_thm": 2, "itauteq": 2, "mani": 2, "ON": 2, "monthm": 2, "fixdef": 2, "elimthm": 2, "out1": 2, "basic": 2, "mk_bounded_fresh": 2, "bang": 2, "bug": 2, "runtim": 2, "ml": 2, "uncom": 2, "doe": 2, "matter": 2, "btw": 2, "ff": 2, "constant_tacl": 2, "ptacl": 2, "all_equals_list": 2, "tac2": 2, "ptac2": 2, "orels": 2, "repeat": 2, "gettimeofdai": 2, "time_aft": 2, "spent": 2, "For": 2, "metavari": 2, "inspect": 2, "pseq": 2, "sym": 2, "eq_true_intro": 2, "tt": 2, "tt_intro": 2, "conj": 2, "andr": 2, "robu": 2, "version": 2, "below": 2, "nil": 2, "andl": 2, "forall_": 2, "mp": 2, "where": 2, "apply_last": 2, "pq": 2, "convers": 2, "al": 2, "strip_const": 2, "expand": 2, "argument": 2, "beta_expand": 2, "seem": 2, "pc": 2, "abs_tac": 2, "sub_tac": 2, "try": 2, "autom": 2, "todo": 2, "our": 2, "rid": 2, "hypothesi": 2, "left": 2, "tri": 2, "search": 2, "space": 2, "via": 2, "focus": 2, "not_": 2, "bit": 2, "long": 2, "want": 2, "produc": 2, "mayb": 2, "automat": 2, "somewher": 2, "els": 2, "exists_": 2, "or_": 2, "and_": 2, "eq_to_impl": 2, "not_i": 2, "sync": 2, "ff_elim": 2, "orr": 2, "orl": 2, "exists_i": 2, "n1": 2, "move": 2, "front": 2, "eq_reflex": 2, "induct": 2, "and_monoton": 2, "or_monoton": 2, "impl_monoton": 2, "not_monoton": 2, "forall_monoton": 2, "exists_monoton": 2, "the_librari": 2, "lstop": 2, "go": 2, "primivit": 2, "oper": 2, "axiomat": 2, "choic": 2, "over": 2, "choos": 2, "connect": 2, "quantifi": 2, "disjoint": 2, "inj1_disj_union": 2, "inj2_disj_union": 2, "case_disj_union": 2, "case_disj_union_inj1": 2, "e1": 2, "e2": 2, "case_disj_union_inj2": 2, "univers": 2, "injection_univ": 2, "ejection_univ": 2, "inject_limit_univ": 2, "eject_limit_univ": 2, "pair_univ": 2, "proj1_univ": 2, "proj2_univ": 2, "inj1_univ": 2, "inj2_univ": 2, "case_univ": 2, "ejection_injection_univ": 2, "eject_inject_limit_univ": 2, "proj1_pair_univ": 2, "p1": 2, "p2": 2, "proj2_pair_univ": 2, "case_univ_inj1": 2, "case_univ_inj2": 2, "or_commut": 2, "or_ff": 2, "or_tt": 2, "or_idempot": 2, "or_associ": 2, "and_commut": 2, "and_tt": 2, "and_ff": 2, "and_idempot": 2, "and_associ": 2, "and_or": 2, "or_and": 2, "ads_or_and": 2, "ads_and_or": 2, "not_or": 2, "not_and": 2, "not_not_not": 2, "impl_not_not": 2, "eq_to_impl_f": 2, "eq_to_impl_b": 2, "properti": 2, "inj": 2, "disj": 2, "pair_univ_inj_l": 2, "x20": 2, "x21": 2, "x22": 2, "x25": 2, "pair_univ_inj_r": 2, "injection_univ_inj": 2, "inj1_univ_inj": 2, "inj2_univ_inj": 2, "not_eq_inj1_inj2_univ": 2, "inj1_disj_union_inj": 2, "inj2_disj_union_inj": 2, "a2": 2, "knaster": 2, "tarski": 2, "j": 2, "in_subseteq": 2, "is_fixpoint": 2, "fixpoint_subseteq_any_fixpoint": 2, "prefixpoint_to_prefixpoint": 2, "fixpoint_is_fixpoint": 2, "found": 2, "recurs": 2, "rec": 2, "acc": 2, "accf": 2, "accf_monoton": 2, "acc_i0": 2, "acc_e0": 2, "acc_": 2, "lt": 2, "acc_i": 2, "well_found": 2, "rec_is_fixpoint": 2, "comment": 2, "requir": 2, "test_appli": 2, "test_apply2": 2, "test_itaut_1": 2, "test_monotone1": 2, "test_monotone2": 2, "test_monotone3": 2, "pnn": 2, "pnnf": 2, "pnnf_monoton": 2, "pnn_i": 2, "pnn_e0": 2, "pnn_e": 2, "pnn_tt": 2, "pnn_not": 2, "ad": 2, "hoc": 2, "fragil": 2, "x15": 2, "pnn_has_two_valu": 2, "elimin": 2, "principl": 2, "in_two": 2, "in_twof": 2, "in_twof_monoton": 2, "in_two_i": 2, "in_two_e0": 2, "in_two_": 2, "in_two_tt": 2, "in_two_ff": 2, "bool2": 2, "myrep2": 2, "myabs2": 2, "myrepabs2": 2, "myabsrep2": 2, "myproprep2": 2, "mytt": 2, "mynot": 2, "mytt_transf": 2, "mynot_transf": 2, "x18": 2, "mybool2_": 2, "x19": 2, "step0": 2, "mynot_mynot_mytt": 2, "step1": 2, "cartesian": 2, "product": 2, "inductive_typ": 2, "abstract": 2, "is_pair": 2, "prod": 2, "prod_rep": 2, "prod_ab": 2, "prod_repab": 2, "prod_absrep": 2, "prod_proprep": 2, "pair": 2, "snd": 2, "usual": 2, "lemma": 2, "natur": 2, "number": 2, "is_nat": 2, "is_natf": 2, "is_nat_monoton": 2, "is_nat_i": 2, "is_nat_e0": 2, "is_nat_": 2, "is_nat_z": 2, "nat_rep": 2, "nat_ab": 2, "nat_repab": 2, "nat_absrep": 2, "nat_proprep": 2, "consequ": 2, "transfer": 2, "nat_": 2, "nat_abs_inj": 2, "nat_rep_inj": 2, "s_inj": 2, "not_equal_z_": 2, "nat_cas": 2, "nat_case_z": 2, "nat_case_": 2, "pred_well_found": 2, "nat_recf": 2, "nat_rec": 2, "nat_rec_ok0": 2, "nat_rec_ok": 2, "arithmet": 2, "sum": 2, "plus_z": 2, "plus_": 2, "plus_n_z": 2, "plus_n_": 2, "plus_comm": 2, "statu": 2, "depend": 2, "converion": 2, "sometim": 2, "diverg": 2, "progress": 2, "myprop": 2, "provid": 2, "wit": 2, "remain": 2, "free": 2, "If": 2, "could": 2, "hand": 2, "would": 2, "need": 2, "symptom": 2, "more": 2, "never": 2, "wai": 2, "atm": 2, "apply_2": 2, "veri": 2, "same": 2, "must": 2, "occurr": 2, "still": 2, "fix": 2, "about": 2, "handl": 2, "discuss": 2, "enrico": 2, "he": 2, "shot": 2, "optim": 2, "possibl": 2, "IN": 2, "unimpl": 2, "onc": 2, "let": 2, "reach": 2, "becom": 2, "user": 2, "hypothes": 2, "least": 2, "But": 2, "better": 2, "bidirect": 2, "successor": 2, "predecessor": 2, "prover": 2, "lambdaprolog": 2, "interfac": 2, "There": 2, "leancop": 2, "prolog": 2, "trick": 2, "small": 2, "formal": 2, "possibli": 2, "everyth": 2, "decis": 2, "procedur": 2, "ring": 2, "inequ": 2, "231": 2, "18": 2, "8433": 2, "malform": 2, "hollight_legaci": 2, "infixr": 2, "126": 2, "arrow": 2, "infixl": 2, "255": 2, "infix": 2, "128": 2, "127": 2, "implic": 2, "iff": 2, "membership": 2, "130": 2, "24": 2, "mixfix": 2, "support": 2, "token": 2, "famili": 2, "identifi": 2, "start": 2, "belong": 2, "preced": 2, "associ": 2, "higher": 2, "than": 2, "here": 2, "tabl": 2, "repres": 2, "symbol": 2, "mark": 2, "cannot": 2, "eg": 2, "while": 2, "increas": 2, "fixiti": 2, "div": 2, "mod": 2, "prefix": 2, "postfix": 2, "stai": 2, "ask": 2, "skip": 2, "120": 2, "As": 2, "facil": 2, "ast": 2, "verifi": 2, "how": 2, "text": 2, "echo": 2, "myformula": 2, "hyp_uvar": 2, "shoud": 2, "31": 2, "62": 2, "089": 2, "impl2": 2, "082": 2, "index2": 2, "iter": 2, "999999": 2, "111": 2, "2318": 2, "627": 2, "io_colon": 2, "lambda": 2, "infer": 2, "simpli": 2, "appl": 2, "288": 2, "186": 2, "234": 2, "330": 2, "095": 2, "lambda2": 2, "41": 2, "087": 2, "lambda3": 2, "termifi": 2, "x16": 2, "x17": 2, "mult": 2, "ten": 2, "thousand": 2, "866": 2, "178": 2, "122": 2, "278": 2, "221": 2, "847": 2, "959": 2, "45": 2, "1020": 2, "104": 2, "293": 2, "list_as_conj": 2, "done": 2, "list_comma": 2, "llam": 2, "dummi": 2, "clause1": 2, "clause2": 2, "prune_arg": 2, "prune_arg2": 2, "prune_arg3": 2, "whatev": 2, "clause3": 2, "so": 2, "alon": 2, "529": 2, "476": 2, "459": 2, "400": 2, "383": 2, "_f": 2, "f_": 2, "c4": 2, "c5": 2, "c6": 2, "112": 2, "llamchr": 2, "resili": 2, "both_or_non": 2, "watch": 2, "becasus": 2, "deal": 2, "dirti": 2, "context": 2, "b2n": 2, "216": 2, "798": 2, "710": 2, "457": 2, "893": 2, "751": 2, "_p": 2, "p_": 2, "xr": 2, "4096": 2, "cmp_term": 2, "time0": 2, "time1": 2, "pr": 2, "broken": 2, "time2": 2, "238042": 2, "052580": 2, "901364": 2, "410": 2, "map_list": 2, "assoc": 2, "671147": 2, "648835": 2, "343164": 2, "670": 2, "map_list_opt": 2, "169061": 2, "472819": 2, "205217": 2, "853": 2, "name_builtin": 2, "named_clauses00": 2, "name1": 2, "named_clauses01": 2, "unabl": 2, "graft": 2, "named_clauses02": 2, "namespaces00": 2, "aux": 2, "rl": 2, "174": 2, "namespaces01": 2, "toto": 2, "insid": 2, "baz": 2, "namespaces02": 2, "namespaces03": 2, "foo1": 2, "foo2": 2, "foo3": 2, "foo4": 2, "187": 2, "168": 2, "nil_con": 2, "con": 2, "notat": 2, "190": 2, "191": 2, "prefixr": 2, "postfixl": 2, "200": 2, "uu": 2, "cd": 2, "132": 2, "zip": 2, "151": 2, "269": 2, "_d": 2, "notation_error": 2, "notation_legaci": 2, "patternunif": 2, "patternunif2": 2, "32": 2, "085": 2, "pi3": 2, "pi5": 2, "bam": 2, "152": 2, "85": 2, "56": 2, "pnf": 2, "transform": 2, "formula": 2, "prenex": 2, "normal": 2, "form": 2, "assum": 2, "classic": 2, "equival": 2, "analyz": 2, "structur": 2, "includ": 2, "modifi": 2, "analysi": 2, "quant_fre": 2, "atom": 2, "termp": 2, "appear": 2, "head": 2, "immedi": 2, "subformula": 2, "proposit": 2, "top": 2, "OF": 2, "f3": 2, "f4": 2, "91": 2, "3225": 2, "688": 2, "475": 2, "855": 2, "891": 2, "93": 2, "3271": 2, "_f4": 2, "f4_": 2, "_f3": 2, "f3_": 2, "_f2": 2, "f2_": 2, "_f1": 2, "f1_": 2, "102": 2, "polymorphic_vari": 2, "langag": 2, "polymorph": 2, "variant": 2, "unari": 2, "funnam": 2, "program": 2, "fun": 2, "distinct": 2, "btl": 2, "ttl": 2, "origti": 2, "check_domain": 2, "check_codomain": 2, "bodi": 2, "is_subset": 2, "is_subset_": 2, "tl": 2, "tl1": 2, "mem_": 2, "check_term": 2, "accord": 2, "ocaml": 2, "ref": 2, "kill": 2, "hindlei": 2, "milner": 2, "interest": 2, "singleton": 2, "up": 2, "trigger": 2, "confus": 2, "between": 2, "mess": 2, "happen": 2, "is_ground": 2, "main1": 2, "Of": 2, "ig": 2, "og": 2, "special": 2, "main2": 2, "ih1": 2, "oh1": 2, "ih2": 2, "oh2": 2, "84": 2, "2748": 2, "2542": 2, "1118": 2, "1008": 2, "3786": 2, "3251": 2, "958": 2, "729": 2, "88": 2, "2860": 2, "80": 2, "2645": 2, "interspers": 2, "35": 2, "1158": 2, "81": 2, "2697": 2, "118": 2, "105": 2, "queen": 2, "less": 2, "neq": 2, "rang": 2, "queens_aux": 2, "unplacedq": 2, "safeq": 2, "unplacedqs1": 2, "not_attack": 2, "not_attack_aux": 2, "dummy1": 2, "dummy2": 2, "first_claus": 2, "no_more_ch": 2, "m1": 2, "tenthousand": 2, "189": 2, "49": 2, "1240": 2, "348": 2, "431": 2, "204": 2, "52": 2, "1389": 2, "649": 2, "_dummy2": 2, "dummy2_": 2, "_dummy1": 2, "dummy1_": 2, "54": 2, "1428": 2, "1471": 2, "1532": 2, "586": 2, "quote_syntax": 2, "builtin": 2, "013": 2, "reduce_cbn": 2, "xxxxxxxxx": 2, "cbn": 2, "y2": 2, "ONE": 2, "six": 2, "twelv": 2, "nine": 2, "five": 2, "285": 2, "211": 2, "563": 2, "_nine": 2, "nine_": 2, "_twelv": 2, "twelve_": 2, "092": 2, "247": 2, "reduce_cbv": 2, "cbv": 2, "r2": 2, "115": 2, "351": 2, "090": 2, "restriction3": 2, "nr": 2, "exit": 2, "442": 2, "restriction4": 2, "069": 2, "restriction5": 2, "restriction6": 2, "yap": 2, "027": 2, "771": 2, "hashtbl": 2, "528": 2, "ineffici": 2, "681": 2, "899": 2, "lvl": 2, "flat": 2, "763": 2, "629": 2, "90": 2, "48": 2, "ocamlopt": 2, "014": 2, "ocamlc": 2, "024": 2, "033": 2, "257": 2, "72": 2, "ulimit": 2, "81920": 2, "newlazi": 2, "lazi": 2, "eager": 2, "78": 2, "00": 2, "auto": 2, "39": 2, "hash": 2, "38": 2, "64": 2, "man": 2, "83": 2, "44": 2, "63": 2, "effici": 2, "ii": 2, "70": 2, "desper": 2, "desperate2": 2, "desperate3": 2, "1827": 2, "1857": 2, "47": 2, "2004": 2, "131": 2, "rev14": 2, "171": 2, "same_term": 2, "self_assign": 2, "succe": 2, "042109": 2, "049706": 2, "765615": 2, "066": 2, "947": 2, "shorten": 2, "177": 2, "shorten2": 2, "shorten_aux": 2, "shorten_aux2": 2, "shorten_builtin": 2, "shorten_tri": 2, "concat1": 2, "escap": 2, "121": 2, "_e": 2, "e_": 2, "_ab": 2, "ab_": 2, "spill_and": 2, "omit": 2, "purpos": 2, "spill_impl": 2, "spill_lam": 2, "trace2": 2, "trace_chr": 2, "trace_cut": 2, "trace_findal": 2, "trail": 2, "outcom": 2, "typeabbrv": 2, "typeabbrev": 2, "typeabbrv1": 2, "typeabbrv10": 2, "tmp": 2, "x30": 2, "x31": 2, "typeabbrv11": 2, "typeabbrv12": 2, "typeabbrv2": 2, "duplic": 2, "abbrevi": 2, "previou": 2, "typeabbrv3": 2, "typeabbrv4": 2, "typeabbrv5": 2, "elpi__compil": 2, "compileerror": 2, "unfold": 2, "typeabbrv6": 2, "unbound": 2, "typeabbrv7": 2, "typeabbrv8": 2, "typeabbrv9": 2, "uminu": 2, "uvar_chr": 2, "mk": 2, "meta": 2, "438": 2, "731": 2, "_x10": 2, "x10_": 2, "variadic_declare_constraint": 2, "tye": 2, "mono": 2, "size": 2, "comma": 2, "integ": 2, "fp": 2, "overbar": 2, "poli": 2, "fresh_": 2, "polyt": 2, "vt": 2, "vg": 2, "tp": 2, "xt": 2, "tq": 2, "76": 2, "1561": 2, "82": 2, "1693": 2, "2038": 2, "2025": 2, "107": 2, "2408": 2, "_tq": 2, "tq_": 2, "w_legaci": 2, "zebra": 2, "elp": 2, "_build": 2, "default": 2, "lib": 2}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"about": 0, "prerequisit": [0, 2], "extens": 0, "build": 0, "welcom": 1, "elpi": 1, "": 1, "document": 1, "api": 1, "playground": 2, "syntax": 2, "regexp": 2, "match": 2, "test": 2, "bed": 2}, "envversion": {"sphinx.domains.c": 3, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 9, "sphinx.domains.index": 1, "sphinx.domains.javascript": 3, "sphinx.domains.math": 2, "sphinx.domains.python": 4, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx.ext.intersphinx": 1, "sphinx": 60}, "alltitles": {"About": [[0, "about"]], "Prerequisites": [[0, "prerequisites"], [2, "prerequisites"]], "Extensions": [[0, "extensions"]], "Building": [[0, "building"]], "Welcome to Elpi\u2019s documentation!": [[1, "welcome-to-elpi-s-documentation"]], "API:": [[1, null]], "Playground": [[2, "playground"]], "Syntax": [[2, "syntax"]], "Regexp Matching": [[2, "regexp-matching"]], "Test Bed": [[2, "test-bed"]]}, "indexentries": {}})
\ No newline at end of file