From 98397d868c6cf083d075c721bad0b7b5124d0745 Mon Sep 17 00:00:00 2001 From: gares Date: Fri, 22 Nov 2024 12:36:25 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20LPCIC/el?= =?UTF-8?q?pi@fb0c159594aab7ac6cade242c7d4bdf88d99ee4e=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- _sources/playground.rst.txt | 34 +++++++++++++++++----------------- playground.html | 34 +++++++++++++++++----------------- searchindex.js | 2 +- 3 files changed, 35 insertions(+), 35 deletions(-) diff --git a/_sources/playground.rst.txt b/_sources/playground.rst.txt index c7282b00..ca039273 100644 --- a/_sources/playground.rst.txt +++ b/_sources/playground.rst.txt @@ -1792,7 +1792,7 @@ Test Bed Success: - Time: 1.861 + Time: 1.813 Constraints: @@ -2167,7 +2167,7 @@ Test Bed Success: - Time: 0.003 + Time: 0.002 Constraints: @@ -2223,7 +2223,7 @@ Test Bed .. code-block:: console - 1.300788 + 0.058018 + 0.923669 + 1.297625 + 0.059550 + 0.953859 .. code-block:: console @@ -2237,7 +2237,7 @@ Test Bed Success: - Time: 2.500 + Time: 2.534 Constraints: @@ -2254,7 +2254,7 @@ Test Bed .. code-block:: console - 6.505476 + 3.030576 + 0.359551 + 6.499013 + 3.073124 + 0.377684 .. code-block:: console @@ -2268,7 +2268,7 @@ Test Bed Success: - Time: 9.902 + Time: 9.956 Constraints: @@ -2285,7 +2285,7 @@ Test Bed .. code-block:: console - 5.804269 + 2.820029 + 0.233417 + 5.767783 + 2.785602 + 0.229297 .. code-block:: console @@ -2299,7 +2299,7 @@ Test Bed Success: - Time: 8.863 + Time: 8.788 Constraints: @@ -2794,7 +2794,7 @@ Test Bed Warning: File "/home/runner/work/elpi/elpi/docs/source/../../tests/sources/pnf.elpi", line 99, column 67, characters 3525-3526: F4 is linear: name it _F4 (discard) or F4_ (fresh variable) - Compilation time: 0.000 + Compilation time: 0.001 Typechecking time: 0.002 @@ -2938,7 +2938,7 @@ Test Bed Success: - Time: 1.574 + Time: 1.600 Constraints: @@ -2972,7 +2972,7 @@ Test Bed .. code-block:: console - 3 + 6 .. code-block:: console @@ -3025,7 +3025,7 @@ Test Bed Success: - Time: 0.239 + Time: 0.254 Constraints: @@ -3064,7 +3064,7 @@ Test Bed Success: - Time: 1.478 + Time: 1.487 Constraints: @@ -3242,7 +3242,7 @@ Test Bed Success: - Time: 0.132 + Time: 0.131 Constraints: @@ -3268,7 +3268,7 @@ Test Bed Success: - Time: 0.130 + Time: 0.136 Constraints: @@ -3337,7 +3337,7 @@ Test Bed .. code-block:: console - 1.135860 + 0.054602 + 0.786017 + 1.137445 + 0.054384 + 0.769559 .. code-block:: console @@ -3351,7 +3351,7 @@ Test Bed Success: - Time: 2.064 + Time: 2.052 Constraints: diff --git a/playground.html b/playground.html index 577eb5e4..71d47d5d 100644 --- a/playground.html +++ b/playground.html @@ -4450,7 +4450,7 @@

Test Bed Success: -Time: 1.861 +Time: 1.813 Constraints: @@ -4918,7 +4918,7 @@

Test Bed Success: -Time: 0.003 +Time: 0.002 Constraints: @@ -5042,7 +5042,7 @@

Test Bed 30 print Time0 "+" Time1 "+" Time2. -
1.300788 + 0.058018 + 0.923669
+
1.297625 + 0.059550 + 0.953859
 

 

 
Parsing time: 0.000
@@ -5053,7 +5053,7 @@ 
Test Bed
 
 Success:
 
-Time: 2.500
+Time: 2.534
 
 Constraints:
 
@@ -5116,7 +5116,7 @@ 
Test Bed
 51  print Time0 "+" Time1 "+" Time2.
 

 

-
6.505476 + 3.030576 + 0.359551
+
6.499013 + 3.073124 + 0.377684
 

 

 
Parsing time: 0.000
@@ -5127,7 +5127,7 @@ 
Test Bed
 
 Success:
 
-Time: 9.902
+Time: 9.956
 
 Constraints:
 
@@ -5185,7 +5185,7 @@ 
Test Bed
 46  print Time0 "+" Time1 "+" Time2.
 

 

-
5.804269 + 2.820029 + 0.233417
+
5.767783 + 2.785602 + 0.229297
 

 

 
Parsing time: 0.000
@@ -5196,7 +5196,7 @@ 
Test Bed
 
 Success:
 
-Time: 8.863
+Time: 8.788
 
 Constraints:
 
@@ -5850,7 +5850,7 @@ 
Test Bed
 Warning: File "/home/runner/work/elpi/elpi/docs/source/../../tests/sources/pnf.elpi", line 99, column 67, characters 3525-3526:
 F4 is linear: name it _F4 (discard) or F4_ (fresh variable)
 
-Compilation time: 0.000
+Compilation time: 0.001
 
 Typechecking time: 0.002
 
@@ -6265,7 +6265,7 @@ 
Test Bed
 
 Success:
 
-Time: 1.574
+Time: 1.600
 
 Constraints:
 
@@ -6297,7 +6297,7 @@ 
Test Bed
 6  R < 10.
 

 

-
3
+
6
 

 

 
Parsing time: 0.000
@@ -6385,7 +6385,7 @@ 
Test Bed
 
 Success:
 
-Time: 0.239
+Time: 0.254
 
 Constraints:
 
@@ -6461,7 +6461,7 @@ 
Test Bed
 
 Success:
 
-Time: 1.478
+Time: 1.487
 
 Constraints:
 
@@ -6718,7 +6718,7 @@ 
Test Bed
 
 Success:
 
-Time: 0.132
+Time: 0.131
 
 Constraints:
 
@@ -6782,7 +6782,7 @@ 
Test Bed
 
 Success:
 
-Time: 0.130
+Time: 0.136
 
 Constraints:
 
@@ -6880,7 +6880,7 @@ 
Test Bed
 31  print Time0 "+" Time1 "+" Time2.
 

 

-
1.135860 + 0.054602 + 0.786017
+
1.137445 + 0.054384 + 0.769559
 

 

 
Parsing time: 0.000
@@ -6891,7 +6891,7 @@ 
Test Bed
 
 Success:
 
-Time: 2.064
+Time: 2.052
 
 Constraints:
 
diff --git a/searchindex.js b/searchindex.js
index e8c4bed7..3c70d8a0 100644
--- a/searchindex.js
+++ b/searchindex.js
@@ -1 +1 @@
-Search.setIndex({"alltitles": {"API:": [[1, null]], "About": [[0, null]], "Building": [[0, "building"]], "Extensions": [[0, "extensions"]], "Playground": [[2, null]], "Prerequisites": [[0, "prerequisites"], [2, "prerequisites"]], "Regexp Matching": [[2, "regexp-matching"]], "Syntax": [[2, "syntax"]], "Test Bed": [[2, "test-bed"]], "Welcome to Elpi\u2019s documentation!": [[1, null]]}, "docnames": ["about", "index", "playground"], "envversion": {"sphinx": 64, "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}, "filenames": ["about.rst", "index.rst", "playground.rst"], "indexentries": {}, "objects": {}, "objnames": {}, "objtypes": {}, "terms": {"": [0, 2], "0": 2, "00": 2, "000": 2, "001": 2, "002": 2, "003": 2, "004": 2, "014": 2, "024": 2, "027": 2, "030576": 2, "033": 2, "054602": 2, "058018": 2, "064": 2, "068": 2, "083": 2, "1": 2, "10": 2, "100": 2, "101": 2, "102": 2, "107": 2, "108": 2, "11": 2, "111": 2, "1112": 2, "1114": 2, "1129": 2, "113": 2, "1132": 2, "1134": 2, "1136": 2, "1169": 2, "1174": 2, "1176": 2, "1181": 2, "12": 2, "120": 2, "1237": 2, "1240": 2, "1276": 2, "1279": 2, "128": 2, "13": 2, "130": 2, "1311": 2, "132": 2, "133": 2, "1333": 2, "1334": 2, "135": 2, "135860": 2, "137": 2, "1388": 2, "1394": 2, "14": 2, "1435": 2, "1436": 2, "1489": 2, "1490": 2, "15": 2, "154": 2, "1541": 2, "1544": 2, "16": 2, "1604": 2, "1609": 2, "1644": 2, "1661": 2, "1666": 2, "17": 2, "18": 2, "1877": 2, "19": 2, "190": 2, "191": 2, "1914": 2, "1915": 2, "1942": 2, "1985": 2, "2": 2, "20": 2, "200": 2, "2005": 2, "2006": 2, "2045": 2, "21": 2, "213": 2, "216": 2, "22": 2, "2253": 2, "2254": 2, "2316": 2, "233417": 2, "2369": 2, "2372": 2, "239": 2, "24": 2, "2429": 2, "2434": 2, "2480": 2, "2481": 2, "25": 2, "253": 2, "2534": 2, "2537": 2, "255": 2, "257": 2, "2594": 2, "2599": 2, "26": 2, "27": 2, "275": 2, "276": 2, "28": 2, "29": 2, "292": 2, "3": 2, "30": 2, "300": 2, "300788": 2, "31": 2, "312": 2, "319": 2, "32": 2, "33": 2, "34": 2, "3477": 2, "3478": 2, "3492": 2, "3493": 2, "35": 2, "3509": 2, "3510": 2, "3525": 2, "3526": 2, "3545": 2, "3546": 2, "359551": 2, "36": 2, "37": 2, "38": 2, "382": 2, "383": 2, "384": 2, "385": 2, "386": 2, "387": 2, "388": 2, "389": 2, "39": 2, "390": 2, "395": 2, "396": 2, "397": 2, "4": 2, "40": 2, "402": 2, "403": 2, "408": 2, "409": 2, "4096": 2, "41": 2, "42": 2, "420": 2, "43": 2, "437": 2, "44": 2, "448": 2, "45": 2, "47": 2, "478": 2, "48": 2, "486": 2, "49": 2, "494": 2, "495": 2, "496": 2, "497": 2, "498": 2, "499": 2, "5": 2, "50": 2, "500": 2, "501": 2, "502": 2, "505476": 2, "507": 2, "508": 2, "509": 2, "51": 2, "514": 2, "515": 2, "517": 2, "52": 2, "520": 2, "521": 2, "528": 2, "53": 2, "533": 2, "549": 2, "55": 2, "56": 2, "565": 2, "57": 2, "574": 2, "580": 2, "59": 2, "6": 2, "60": 2, "61": 2, "62": 2, "623": 2, "628": 2, "629": 2, "63": 2, "637": 2, "64": 2, "65": 2, "657": 2, "66": 2, "660": 2, "67": 2, "671": 2, "676": 2, "681": 2, "683": 2, "688": 2, "7": 2, "70": 2, "712": 2, "719": 2, "72": 2, "728": 2, "73": 2, "74": 2, "75": 2, "756": 2, "76": 2, "761": 2, "763": 2, "77": 2, "771": 2, "78": 2, "781": 2, "786017": 2, "79": 2, "795": 2, "797": 2, "8": 2, "80": 2, "804269": 2, "81": 2, "819": 2, "81920": 2, "820029": 2, "821": 2, "83": 2, "85": 2, "853": 2, "858": 2, "861": 2, "863": 2, "87": 2, "88": 2, "89": 2, "899": 2, "9": 2, "90": 2, "902": 2, "923669": 2, "93": 2, "96": 2, "961": 2, "964": 2, "97": 2, "98": 2, "99": 2, "999999": 2, "A": 2, "As": 2, "But": 2, "FOR": 2, "For": 2, "IN": 2, "If": 2, "In": 2, "It": 2, "No": 2, "OF": 2, "ON": 2, "ONE": 2, "Of": 2, "On": [0, 2], "Or": 0, "The": 2, "There": 2, "To": [0, 2], "_": 2, "_a": 2, "_ab": 2, "_b": 2, "_build": 2, "_c": 2, "_d": 2, "_dummy1": 2, "_dummy2": 2, "_e": 2, "_f": 2, "_f1": 2, "_f2": 2, "_f3": 2, "_f4": 2, "_foo": 2, "_g": 2, "_nine": 2, "_t": 2, "_tq": 2, "_twelv": 2, "_v": 2, "_x": 2, "_x0": 2, "_x01": 2, "_x1": 2, "_x10": 2, "_x2": 2, "_x3": 2, "_x4": 2, "_x5": 2, "_y": 2, "_z": 2, "a1": 2, "a2": 2, "a_": 2, "ab": 2, "ab_": 2, "abbrevi": 2, "abort": 2, "about": 2, "abs_tac": 2, "absrep": 2, "absreptyp": 2, "abstract": 2, "abstyp": 2, "acc": 2, "acc_": 2, "acc_e0": 2, "acc_i": 2, "acc_i0": 2, "accf": 2, "accf_monoton": 2, "accord": 2, "accumul": 2, "accumulate_twice1": 2, "accumulate_twice2": 2, "ack": 2, "ackermann": 2, "ad": 2, "add": 2, "adepth": 2, "adj": 2, "ads_and_or": 2, "ads_or_and": 2, "after": 2, "al": 2, "all": 2, "all_equals_list": 2, "alon": 2, "alreadi": 2, "also": 2, "altern": 2, "an": [0, 2], "analysi": 2, "analyz": 2, "and_": 2, "and_associ": 2, "and_commut": 2, "and_ff": 2, "and_idempot": 2, "and_monoton": 2, "and_or": 2, "and_tt": 2, "andl": 2, "andr": 2, "ani": [0, 2], "answer": 2, "app": 2, "appear": 2, "append": 2, "appl": 2, "appli": 2, "applic": 2, "apply_2": 2, "apply_last": 2, "applyth": 2, "appuvar": 2, "apredf": 2, "apt": 0, "ar": [0, 2], "arg": 2, "argument": 2, "arithmet": 2, "ariti": 2, "around": 2, "arr": 2, "as_1": 2, "as_2": 2, "as_3": 2, "asclaus": 2, "ask": 2, "assert": 2, "assoc": 2, "associ": 2, "assum": 2, "assumpt": 2, "ast": 2, "atisym": 2, "atm": 2, "atom": 2, "auto": 2, "auto_monoton": 2, "autom": 2, "automat": 2, "aux": 2, "avail": 2, "avoid": 2, "axiom": 2, "axiomat": 2, "b": 2, "b1": 2, "b2": 2, "b2n": 2, "b_": 2, "backchain": 2, "backtrack": 2, "bad": 2, "bam": 2, "bang": 2, "bar": 2, "base": [0, 2], "basic": 2, "baz": 2, "bdepth": 2, "becasus": 2, "becaus": 2, "becom": 2, "befor": [0, 2], "belong": 2, "below": 2, "beta": 2, "beta_expand": 2, "better": 2, "between": 2, "bi": 2, "bidirect": 2, "bind": 2, "bit": 2, "block": 2, "bo": 2, "bodi": 2, "bool": 2, "bool2": 2, "both": [0, 2], "both_or_non": 2, "bound": 2, "box": 2, "brain": 2, "branch": 2, "broken": 2, "btl": 2, "btw": 2, "bug": 2, "build": 2, "build_pred": 2, "build_quantified_pred": 2, "built": 2, "builtin": 2, "c": 2, "c0": 2, "c1": 2, "c2": 2, "c3": 2, "c4": 2, "c5": 2, "c6": 2, "call": 2, "callback_prov": 2, "can": [0, 2], "cannot": 2, "canon": 2, "canonicaltac": 2, "captur": 2, "cardin": 2, "cartesian": 2, "case": 2, "case_disj_union": 2, "case_disj_union_inj1": 2, "case_disj_union_inj2": 2, "case_univ": 2, "case_univ_inj1": 2, "case_univ_inj2": 2, "cast": 2, "cbn": 2, "cbv": 2, "cd": 2, "cert": 2, "certif": 2, "chang": 2, "charact": 2, "check": 2, "check1": 2, "check1axm": 2, "check1decl": 2, "check1def": 2, "check1nbt": 2, "check1thm": 2, "check_codomain": 2, "check_domain": 2, "check_hyp": 2, "check_term": 2, "choic": 2, "choos": 2, "chr": 2, "chr_nokei": 2, "chr_nokey2": 2, "chr_not_cliqu": 2, "chr_sem": 2, "chrgcd": 2, "chrleq": 2, "classic": 2, "claus": 2, "clause1": 2, "clause2": 2, "clause3": 2, "close": 2, "cmp_term": 2, "code": 2, "column": 2, "come": 0, "comma": 2, "command": 2, "comment": 2, "common": 2, "commun": 0, "compat": 2, "compil": 2, "complet": 2, "con": 2, "concat1": 2, "confus": 2, "conj": 2, "conj2": 2, "conjunct": 2, "connect": 2, "consequ": 2, "consist": 2, "consol": 2, "const": 2, "constant": 2, "constant_tacl": 2, "constraint": 2, "cont": 2, "contain": 2, "content": 2, "context": 2, "contnext": 2, "conv": 2, "convention": 2, "converion": 2, "convers": 2, "copi": 2, "coq": 0, "correctli": 2, "could": 2, "counter": 2, "creat": [0, 2], "cross": 0, "cs_": 2, "cscript": 2, "ct": 2, "ctx": 2, "ctx_load": 2, "ctxconstr": 2, "current": [0, 2], "cut": 2, "cut2": 2, "cut3": 2, "cut4": 2, "cut5": 2, "cut6": 2, "cutth": 2, "d": 2, "d1": 2, "d11": 2, "d2": 2, "d22": 2, "d3": 2, "d33": 2, "d_": 2, "daemon": 2, "damag": 2, "data": 2, "dd": 2, "deal": 2, "debian": 0, "debprint": 2, "debug": 2, "debuggin": 2, "decis": 2, "decl": 2, "declar": 2, "declare_constraint": 2, "deep_index": 2, "def": 2, "def0": 2, "default": 2, "defin": 2, "definit": 2, "deftac": 2, "deftacl": 2, "delai": 2, "delay_outside_frag": 2, "denot": 2, "depend": 2, "deprec": 2, "depth": 2, "depth_tac": 2, "desper": 2, "desperate2": 2, "desperate3": 2, "develop": 2, "diagnost": 2, "did": 2, "differ": 2, "direct": 2, "directli": 0, "directori": 0, "dirti": 2, "discard": 2, "discuss": 2, "disj": 2, "disj_union": 2, "disjoint": 2, "distinct": 2, "distinct_nam": 2, "distrib": 0, "div": 2, "diverg": 2, "do": 2, "doc": [0, 2], "document": [0, 2], "doe": 2, "doesn": 2, "done": 2, "doom": 2, "doubl": 2, "down": 2, "drop": 2, "due": 2, "dummi": 2, "dummy1": 2, "dummy1_": 2, "dummy2": 2, "dummy2_": 2, "dune": 2, "duplic": 2, "e": [0, 2], "e1": 2, "e2": 2, "e_": 2, "eager": 2, "echo": 2, "effici": 2, "eg": 2, "either": 0, "eject_inject_limit_univ": 2, "eject_limit_univ": 2, "ejection_injection_univ": 2, "ejection_univ": 2, "element": 2, "elimin": 2, "elimthm": 2, "elp": 2, "elpi": 2, "elpi_api": 2, "elpi_only_llam": 2, "els": 2, "empti": 2, "en": 0, "end": 2, "end_com": 2, "end_of_proof": 2, "engin": 2, "enrico": 2, "enter": 2, "env": 2, "eq": 2, "eq_reflex": 2, "eq_to_impl": 2, "eq_to_impl_b": 2, "eq_to_impl_f": 2, "eq_true_intro": 2, "equal": 2, "equival": 2, "erro": 2, "error": 2, "escap": 2, "eta": 2, "eta_a": 2, "eval": 2, "evalu": 2, "even": 2, "everyth": 2, "exampl": 2, "except": 2, "exec": 2, "exist": 2, "existence_condit": 2, "exists_": 2, "exists_i": 2, "exists_monoton": 2, "exit": 2, "exp": 2, "expand": 2, "expect": 2, "explicitli": 0, "export": 2, "ext": 0, "extend": 2, "extern": 0, "extra": 2, "f": 2, "f1": 2, "f1_": 2, "f2": 2, "f2_": 2, "f3": 2, "f3_": 2, "f4": 2, "f4_": 2, "f_": 2, "facil": 2, "fail": 2, "failur": 2, "fallback": 0, "fals": 2, "famili": 2, "fatal": 2, "ff": 2, "ff_elim": 2, "file": [0, 2], "filter": 2, "find": 2, "findal": 2, "first": 2, "first_claus": 2, "five": 2, "fix": 2, "fixdef": 2, "fixiti": 2, "fixpoint": 2, "fixpoint_is_fixpoint": 2, "fixpoint_is_prefixpoint": 2, "fixpoint_subseteq_any_fixpoint": 2, "fixpoint_subseteq_any_prefixpoint": 2, "flat": 2, "flexibl": 2, "flush": 2, "fn": 2, "focus": 2, "fold": 2, "fold2_append": 2, "follow": [0, 2], "foo": 2, "foo1": 2, "foo2": 2, "foo3": 2, "foo4": 2, "foral": 2, "forall_": 2, "forall_i": 2, "forall_monoton": 2, "forc": 2, "form": 2, "formal": 2, "formed": 2, "formula": 2, "found": 2, "four": 2, "fp": 2, "fr": 0, "fragil": 2, "fragment": 2, "fragment_exit": 2, "fragment_exit2": 2, "fragment_exit3": 2, "free": 2, "fresh": 2, "fresh_": 2, "from": 2, "front": 2, "frozen": 2, "fst": 2, "ft": 2, "fun": 2, "function": 2, "funnam": 2, "g": [0, 2], "g1": 2, "g2": 2, "g_": 2, "gamma": 2, "gamma1": 2, "gamma2": 2, "gc": 2, "gcd": 2, "gener": [0, 2], "general_cas": 2, "general_case2": 2, "general_case3": 2, "get": 2, "gettimeofdai": 2, "github": 0, "githubpag": 0, "global": 2, "go": 2, "goal": 2, "goaltact": 2, "group": 2, "gx": 2, "gy": 2, "h": 2, "h1": 2, "h2": 2, "ha": 2, "hack": 2, "halt": 2, "hand": 2, "handl": 2, "happen": 2, "hard": 2, "hash": 2, "hashtbl": 2, "have": [0, 2], "hc_interp": 2, "hd": 2, "hdclaus": 2, "he": 2, "head": 2, "heap_discard": 2, "helper": 0, "henc": 2, "here": 2, "higher": 2, "hindlei": 2, "ho": 2, "hoc": 2, "hol": 2, "hollight": 2, "hollight_legaci": 2, "home": 2, "hook": 2, "horn": 2, "how": 2, "html": 0, "http": 0, "hurt": 2, "hyp": 2, "hyp_uvar": 2, "hypothes": 2, "hypothesi": 2, "hypsuchthat": 2, "i": [0, 2], "id": 2, "idempot": 2, "identifi": 2, "ig": 2, "ign": 2, "ignor": 2, "ih1": 2, "ih2": 2, "ii": 2, "illustr": 2, "immedi": 2, "imp": 2, "impl": 2, "impl2": 2, "impl_monoton": 2, "impl_not_not": 2, "implement": 2, "implic": 2, "implicit": 2, "in_subseteq": 2, "in_two": 2, "in_two_": 2, "in_two_e0": 2, "in_two_ff": 2, "in_two_i": 2, "in_two_tt": 2, "in_twof": 2, "in_twof_monoton": 2, "includ": 2, "incompat": 2, "increas": 2, "index": 2, "index2": 2, "induct": 2, "inductive_def": 2, "inductive_def_pkg": 2, "inductive_typ": 2, "ineffici": 2, "inequ": 2, "infer": 2, "infix": 2, "infixl": 2, "infixr": 2, "inj": 2, "inj1_disj_union": 2, "inj1_disj_union_inj": 2, "inj1_univ": 2, "inj1_univ_inj": 2, "inj2_disj_union": 2, "inj2_disj_union_inj": 2, "inj2_univ": 2, "inj2_univ_inj": 2, "inject": [0, 2], "inject_limit_univ": 2, "injection_univ": 2, "injection_univ_inj": 2, "input": 2, "inria": 0, "insid": 2, "inspect": 2, "instal": [0, 2], "instead": [0, 2], "int": 2, "int_tac": 2, "integ": 2, "inter": 2, "interact": 2, "interactive_tac": 2, "interest": 2, "interfac": 2, "interpret": 2, "intersphinx": 0, "introspect": 0, "introthm": 2, "inv": 2, "io_colon": 2, "is_fixpoint": 2, "is_ground": 2, "is_nat": 2, "is_nat_": 2, "is_nat_e0": 2, "is_nat_i": 2, "is_nat_monoton": 2, "is_nat_z": 2, "is_natf": 2, "is_pair": 2, "is_subset": 2, "is_subset_": 2, "itac": 2, "itaut": 2, "itauteq": 2, "iter": 2, "its": [0, 2], "j": 2, "just": 2, "jwintz": 2, "k": 2, "k1": 2, "k2": 2, "kernel": 2, "keyword": 2, "kill": 2, "kind": 2, "knaster": 2, "known": 2, "ko": 2, "ko1": 2, "ko2": 2, "l": 2, "l1": 2, "l2": 2, "lam": 2, "lambda": 2, "lambda2": 2, "lambda3": 2, "lambdaprolog": 2, "land_tac": 2, "langag": 2, "lappli": 2, "lapply_last": 2, "last": 2, "lazi": 2, "leancop": 2, "least": 2, "left": 2, "legaci": 1, "lemma": 2, "len": 2, "length": 2, "leq": 2, "less": 2, "let": 2, "level": 2, "lforal": 2, "lforall_last": 2, "lib": 2, "librari": 2, "light": 2, "like": 2, "line": 2, "linear": 2, "link": 0, "list": 2, "list_as_conj": 2, "list_comma": 2, "list_iter_rev": 2, "list_map": 2, "liter": 2, "literalinclud": 2, "llam": 2, "llamchr": 2, "local": 2, "logic": 2, "long": 2, "longer": 2, "look": 2, "loop": 2, "lost": 2, "lower": 2, "lprolog": 2, "lstop": 2, "lt": 2, "ltn": 2, "lvl": 2, "lx": 2, "ly": 2, "m": 2, "m1": 2, "m2": 2, "macro": 2, "mai": 2, "main": 2, "main1": 2, "main2": 2, "make": [0, 2], "makefil": 0, "man": 2, "manag": 0, "mani": 2, "map": 2, "map_list": 2, "map_list_opt": 2, "mark": 2, "master": 0, "match": 0, "matter": 2, "mayb": 2, "mean": 2, "meant": 0, "mem": 2, "mem_": 2, "memb": 2, "merg": 2, "mess": 2, "messag": 2, "meta": 2, "metavari": 2, "milner": 2, "miss": 2, "mistak": 2, "mixfix": 2, "mk": 2, "mk_bounded_fresh": 2, "mk_constant_list": 2, "mk_intro_thm": 2, "mk_list_of_bounded_fresh": 2, "mk_script": 2, "ml": 2, "mod": 2, "mode": 2, "modifi": 2, "modul": [0, 2], "mono": 2, "monoton": 2, "monthm": 2, "more": 2, "move": 2, "mp": 2, "much": 2, "mult": 2, "must": 2, "myabs2": 2, "myabsrep2": 2, "mybool2_": 2, "myformula": 2, "mynot": 2, "mynot_mynot_mytt": 2, "mynot_transf": 2, "myprop": 2, "myproprep2": 2, "myrep2": 2, "myrepabs2": 2, "mytt": 2, "mytt_transf": 2, "n": 2, "n1": 2, "n2": 2, "name": [0, 2], "name1": 2, "name_builtin": 2, "named_clauses00": 2, "named_clauses01": 2, "named_clauses02": 2, "namespac": 2, "namespaces00": 2, "namespaces01": 2, "namespaces02": 2, "namespaces03": 2, "nat": 2, "nat_": 2, "nat_ab": 2, "nat_abs_inj": 2, "nat_absrep": 2, "nat_cas": 2, "nat_case_": 2, "nat_case_z": 2, "nat_proprep": 2, "nat_rec": 2, "nat_rec_ok": 2, "nat_rec_ok0": 2, "nat_recf": 2, "nat_rep": 2, "nat_rep_inj": 2, "nat_repab": 2, "natur": 2, "need": 2, "neq": 2, "never": 2, "new": 2, "new2": 2, "new_basic_typ": 2, "new_certif": 2, "new_interactive_tac": 2, "new_tac": 2, "newcom": 2, "newl": 2, "newlazi": 2, "newt": 2, "next": 2, "next_object": 2, "next_tact": 2, "next_tactic0": 2, "nil": 2, "nil_con": 2, "nine": 2, "nine_": 2, "no_more_ch": 2, "nojekyl": 0, "non": 2, "non_interactive_tac": 2, "normal": 2, "not_": 2, "not_and": 2, "not_attack": 2, "not_attack_aux": 2, "not_defin": 2, "not_eq_inj1_inj2_univ": 2, "not_equal_z_": 2, "not_i": 2, "not_monoton": 2, "not_not_not": 2, "not_or": 2, "notat": 2, "notation_error": 2, "notation_legaci": 2, "note": 2, "noth": 2, "now": 2, "nr": 2, "num": 2, "number": 2, "o": 2, "object": [0, 2], "ocaml": 2, "ocamlc": 2, "ocamlopt": 2, "occur": 2, "occurr": 2, "odd": 2, "og": 2, "oh1": 2, "oh2": 2, "ok": 2, "old": 2, "omit": 2, "onc": 2, "one": [0, 2], "ones": 2, "onli": 2, "opam": 2, "oper": 2, "opr": 2, "optim": 2, "option": [1, 2], "or_": 2, "or_and": 2, "or_associ": 2, "or_commut": 2, "or_ff": 2, "or_idempot": 2, "or_monoton": 2, "or_tt": 2, "order": 2, "orels": 2, "org": 0, "origti": 2, "orl": 2, "orr": 2, "otac": 2, "other": [0, 2], "other_tac": 2, "otherwis": 2, "our": 2, "out": 2, "out1": 2, "outcom": 2, "output": 2, "outs2": 2, "outsid": 2, "over": 2, "overbar": 2, "own": 0, "p": 2, "p1": 2, "p2": 2, "p_tactic": 2, "pa": 2, "packag": [0, 2], "page": [0, 2], "pair": 2, "pair_univ": 2, "pair_univ_inj_l": 2, "pair_univ_inj_r": 2, "param": 2, "pars": 2, "parse_axiom": 2, "parse_def": 2, "parse_inductive_def_spec": 2, "parse_nbt": 2, "parse_obj": 2, "parse_thm": 2, "parser": [1, 2], "parsetac": 2, "parseterm": 2, "pass": 2, "path": 2, "pathfroma": 2, "pattern": 2, "patternunif": 2, "patternunif2": 2, "pb": 2, "pc": 2, "pcanonicaltac": 2, "pdef": 2, "perp": 2, "pf": 2, "pg": 2, "pgamma": 2, "pgoal": 2, "ph": 2, "pi": 2, "pi3": 2, "pi5": 2, "pip": 0, "pl": 2, "place": 0, "playground": 0, "pleas": 2, "plu": 2, "plugin": 0, "plus_": 2, "plus_comm": 2, "plus_n_": 2, "plus_n_z": 2, "plus_z": 2, "pnf": 2, "pnn": 2, "pnn_e": 2, "pnn_e0": 2, "pnn_has_two_valu": 2, "pnn_i": 2, "pnn_not": 2, "pnn_tt": 2, "pnnf": 2, "pnnf_monoton": 2, "point": 0, "poli": 2, "polymorph": 2, "polymorphic_vari": 2, "polyt": 2, "possibl": 2, "possibli": 2, "postfix": 2, "postfixl": 2, "pp": 2, "pp_tactic": 2, "ppp": 2, "ppptac": 2, "pptac": 2, "ppterm": 2, "pq": 2, "pr": 2, "preced": 2, "pred": 2, "pred_": 2, "pred_e0": 2, "pred_i": 2, "pred_well_found": 2, "predecessor": 2, "predf": 2, "predf_mon": 2, "predf_monoton": 2, "predic": 2, "prefix": 2, "prefixpoint_to_prefixpoint": 2, "prefixr": 2, "prenex": 2, "prep": 2, "preph": 2, "prephtyp": 2, "pretti": 2, "previou": 2, "primivit": 2, "principl": 2, "print": 2, "print_constraint": 2, "print_sequ": 2, "printer": 2, "probabl": 2, "problem": 2, "procedur": 2, "process_constructor": 2, "prod": 2, "prod_ab": 2, "prod_absrep": 2, "prod_proprep": 2, "prod_rep": 2, "prod_repab": 2, "produc": 2, "product": 2, "prog": 2, "program": 2, "progress": 2, "proj1_pair_univ": 2, "proj1_univ": 2, "proj2_pair_univ": 2, "proj2_univ": 2, "project": 0, "prolog": 2, "proof": 2, "prop": 2, "propag": 2, "properti": 2, "proposit": 2, "provabl": 2, "prove": 2, "prove_fix_elim_thm": 2, "prove_fix_intro_thm": 2, "prove_intro_thm": 2, "prove_monotonicity_thm": 2, "prover": 2, "provid": 2, "prune": 2, "prune_arg": 2, "prune_arg2": 2, "prune_arg3": 2, "pscript": 2, "pseq": 2, "pst": 2, "psttac": 2, "ptac": 2, "ptac1": 2, "ptac2": 2, "ptacl": 2, "ptacn": 2, "pty": 2, "ptybo": 2, "ptyp": 2, "ptype": 2, "publish": 0, "purpos": 2, "put": 2, "put_bind": 2, "px": 2, "py": 2, "python3": 0, "q": 2, "quant_fre": 2, "quantifi": 2, "quater": 2, "queen": 2, "queens_aux": 2, "queri": 2, "quote_syntax": 2, "r": 2, "r2": 2, "rand_tac": 2, "random": 2, "rang": 2, "rator_tac": 2, "re": 2, "reach": 2, "read": 2, "read_cmd": 2, "read_in_context": 2, "readterm": 2, "realiz": 2, "realli": 2, "rec": 2, "rec_is_fixpoint": 2, "recogn": 2, "recurs": 2, "reduc": 2, "reduce_cbn": 2, "reduce_cbv": 2, "reduct": 2, "ref": 2, "refer": [0, 2], "refl": 2, "refman": 0, "regress": 2, "relev": 2, "remain": 2, "remov": 2, "rep": 2, "repab": 2, "repabstyp": 2, "repeat": 2, "repres": 2, "reptyp": 2, "requir": 2, "resili": 2, "resolut": 0, "rest": 2, "restrict": 2, "restriction3": 2, "restriction4": 2, "restriction5": 2, "restriction6": 2, "restructuredtext": 2, "result": 2, "resumpt": 2, "reterm": 2, "retriev": 2, "return": 2, "rev": 2, "rev14": 2, "rid": 2, "right": 2, "ring": 2, "rl": 2, "robu": 2, "role": 0, "root": 0, "rtd": 0, "rule": 2, "run": 2, "runner": 2, "runtim": 2, "s1": 2, "s2": 2, "s_inj": 2, "safe_list_map": 2, "safeq": 2, "same": 2, "same_term": 2, "same_var": 2, "script": 2, "search": 2, "section": 0, "see": [0, 2], "seem": 2, "select": 2, "self": 0, "self_assign": 2, "self_init": 2, "semant": 2, "seq": 2, "sequent": 2, "set": 2, "shorten": 2, "shorten2": 2, "shorten_aux": 2, "shorten_aux2": 2, "shorten_builtin": 2, "shorten_tri": 2, "shot": 2, "shoud": 2, "should": 2, "sigma": 2, "silenc": 2, "simpl": 2, "simpli": 2, "sinc": 2, "singleton": 2, "six": 2, "size": 2, "skip": 2, "slow": 2, "small": 2, "snd": 2, "snippet": 2, "so": 2, "solv": 2, "some": 2, "sometim": 2, "somewher": 2, "sourc": [0, 2], "space": 2, "special": 2, "spent": 2, "sphinx": [0, 2], "spill_and": 2, "spill_impl": 2, "spill_lam": 2, "spy": 2, "src": 2, "src263": 2, "src265": 2, "st": 2, "stack": 0, "stai": 2, "standard": 2, "start": 2, "state": 2, "state_fixpoint_def": 2, "statement": 2, "statu": 2, "std": 2, "std_in": 2, "std_out": 2, "stderr": 2, "stdout": 2, "step0": 2, "step1": 2, "still": 2, "stm": 2, "stop": 2, "string": 2, "strip_const": 2, "structur": 2, "sttac": 2, "sub_tac": 2, "subformula": 2, "subproof": 2, "subset": 2, "subseteq": 2, "subst": 2, "substitut": 2, "succ": 2, "succe": 2, "success": 2, "successor": 2, "sum": 2, "super": 2, "support": 2, "sure": [0, 2], "suspend": 2, "sym": 2, "symbol": 2, "symptom": 2, "sync": 2, "system": 0, "t": 2, "t1": 2, "t1_": 2, "t2": 2, "t2_": 2, "t_": 2, "tabl": 2, "tac": 2, "tac1": 2, "tac2": 2, "tacl": 2, "tacn": 2, "tactic": 2, "target": 0, "tarski": 2, "tc": 2, "temporarili": 2, "ten": 2, "tenthousand": 2, "ter": 2, "term": 2, "termifi": 2, "termp": 2, "test1": 2, "test2": 2, "test3": 2, "test4": 2, "test5": 2, "test_appli": 2, "test_apply2": 2, "test_itaut_1": 2, "test_monotone1": 2, "test_monotone2": 2, "test_monotone3": 2, "text": 2, "teyju": 2, "tgt": 2, "th": 2, "than": 2, "the_librari": 2, "thei": 2, "them": 2, "theme": 0, "thenl": 2, "thenll": 2, "theorem": 2, "therefor": 2, "thi": [0, 2], "third": 2, "thm": 2, "thousand": 2, "three": 2, "through": 0, "time": 2, "time0": 2, "time1": 2, "time2": 2, "time_aft": 2, "tl": 2, "tl1": 2, "tm": 2, "tmp": 2, "todo": 2, "token": 2, "too": 2, "top": 2, "toplevel": 2, "toplevel_loop": 2, "toto": 2, "tp": 2, "trace": 2, "trace2": 2, "trace_chr": 2, "trace_cut": 2, "trace_findal": 2, "trail": 2, "tran": 2, "transfer": 2, "transform": 2, "tree": 0, "tri": 2, "trick": 2, "tricki": 2, "trigger": 2, "tru": 2, "true": 2, "true_then_fals": 2, "trust": 2, "try": 2, "try_claus": 2, "tt": 2, "tt_intro": 2, "ttl": 2, "turn": 2, "twelv": 2, "twelve_": 2, "two": 2, "tx": 2, "ty": 2, "tybo": 2, "tye": 2, "typ": 2, "typdef": 2, "type": 2, "typeabbrev": 2, "typeabbrv": 2, "typeabbrv1": 2, "typeabbrv10": 2, "typeabbrv11": 2, "typeabbrv12": 2, "typeabbrv2": 2, "typeabbrv3": 2, "typeabbrv4": 2, "typeabbrv5": 2, "typeabbrv6": 2, "typeabbrv7": 2, "typeabbrv8": 2, "typeabbrv9": 2, "typecheck": 2, "u": 2, "u1": 2, "u2": 2, "uid_priv": 2, "ulimit": 2, "ultim": 2, "uminu": 2, "unabl": 2, "unari": 2, "uncom": 2, "undeclar": 2, "unif": 2, "unif_1": 2, "unif_2": 2, "unif_zero": 2, "unifi": 2, "unimpl": 2, "union": 2, "univ": 2, "univers": 2, "unknown": 2, "unplacedq": 2, "unplacedqs1": 2, "unsaf": 2, "untrust": 2, "untyp": 2, "up": 2, "update_certif": 2, "us": [0, 2], "usag": 0, "user": 2, "usual": 2, "util": 2, "uu": 2, "uvar": 2, "uvar_1": 2, "uvar_2": 2, "uvar_3": 2, "uvar_4": 2, "uvar_5": 2, "uvar_6": 2, "uvar_chr": 2, "v": 2, "v1": 2, "v2": 2, "v_": 2, "valid": 2, "var": 2, "variabl": 2, "variad": 2, "variadic_declare_constraint": 2, "variant": 2, "veri": 2, "verifi": 2, "version": 2, "vg": 2, "via": 2, "vim": 2, "visual": 0, "vt": 2, "w": 2, "w_legaci": 2, "wa": 2, "wai": 2, "want": 2, "warn": 2, "watch": 2, "we": 2, "welcom": 2, "well": 2, "well_found": 2, "wgamma": 2, "what": 2, "whatev": 2, "when": 2, "where": 2, "which": [0, 2], "while": 2, "why": 2, "wit": 2, "within": 2, "without": 2, "wl": 2, "work": 2, "would": 2, "write": 2, "wrong": 2, "ww": 2, "www": 0, "x": 2, "x0": 2, "x01": 2, "x01_": 2, "x0_": 2, "x1": 2, "x10": 2, "x10_": 2, "x11": 2, "x12": 2, "x13": 2, "x14": 2, "x15": 2, "x16": 2, "x17": 2, "x18": 2, "x19": 2, "x1_": 2, "x2": 2, "x20": 2, "x21": 2, "x22": 2, "x23": 2, "x24": 2, "x25": 2, "x26": 2, "x2_": 2, "x3": 2, "x3_": 2, "x4": 2, "x4_": 2, "x5": 2, "x5_": 2, "x6": 2, "x7": 2, "x8": 2, "x9": 2, "x_": 2, "xa": 2, "xcon": 2, "xnil": 2, "xr": 2, "xt": 2, "xtac": 2, "xx": 2, "xxx": 2, "xxxxxxxxx": 2, "y": 2, "y2": 2, "y_": 2, "yap": 2, "yield": 2, "you": 2, "your": 2, "ysx": 2, "yx": 2, "yy": 2, "z": 2, "z_": 2, "zebra": 2, "zero": 2, "\u03bbprolog": 2}, "titles": ["About", "Welcome to Elpi\u2019s documentation!", "Playground"], "titleterms": {"": 1, "about": 0, "api": 1, "bed": 2, "build": 0, "document": 1, "elpi": 1, "extens": 0, "match": 2, "playground": 2, "prerequisit": [0, 2], "regexp": 2, "syntax": 2, "test": 2, "welcom": 1}})
\ No newline at end of file
+Search.setIndex({"alltitles": {"API:": [[1, null]], "About": [[0, null]], "Building": [[0, "building"]], "Extensions": [[0, "extensions"]], "Playground": [[2, null]], "Prerequisites": [[0, "prerequisites"], [2, "prerequisites"]], "Regexp Matching": [[2, "regexp-matching"]], "Syntax": [[2, "syntax"]], "Test Bed": [[2, "test-bed"]], "Welcome to Elpi\u2019s documentation!": [[1, null]]}, "docnames": ["about", "index", "playground"], "envversion": {"sphinx": 64, "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}, "filenames": ["about.rst", "index.rst", "playground.rst"], "indexentries": {}, "objects": {}, "objnames": {}, "objtypes": {}, "terms": {"": [0, 2], "0": 2, "00": 2, "000": 2, "001": 2, "002": 2, "004": 2, "014": 2, "024": 2, "027": 2, "033": 2, "052": 2, "054384": 2, "059550": 2, "068": 2, "073124": 2, "083": 2, "1": 2, "10": 2, "100": 2, "101": 2, "102": 2, "107": 2, "108": 2, "11": 2, "111": 2, "1112": 2, "1114": 2, "1129": 2, "113": 2, "1132": 2, "1134": 2, "1136": 2, "1169": 2, "1174": 2, "1176": 2, "1181": 2, "12": 2, "120": 2, "1237": 2, "1240": 2, "1276": 2, "1279": 2, "128": 2, "13": 2, "131": 2, "1311": 2, "133": 2, "1333": 2, "1334": 2, "135": 2, "136": 2, "137": 2, "137445": 2, "1388": 2, "1394": 2, "14": 2, "1435": 2, "1436": 2, "1489": 2, "1490": 2, "15": 2, "154": 2, "1541": 2, "1544": 2, "16": 2, "1604": 2, "1609": 2, "1644": 2, "1661": 2, "1666": 2, "17": 2, "18": 2, "1877": 2, "19": 2, "190": 2, "191": 2, "1914": 2, "1915": 2, "1942": 2, "1985": 2, "2": 2, "20": 2, "200": 2, "2005": 2, "2006": 2, "2045": 2, "21": 2, "213": 2, "216": 2, "22": 2, "2253": 2, "2254": 2, "229297": 2, "2316": 2, "2369": 2, "2372": 2, "24": 2, "2429": 2, "2434": 2, "2480": 2, "2481": 2, "25": 2, "253": 2, "2534": 2, "2537": 2, "254": 2, "255": 2, "257": 2, "2594": 2, "2599": 2, "26": 2, "27": 2, "275": 2, "276": 2, "28": 2, "29": 2, "292": 2, "297625": 2, "3": 2, "30": 2, "300": 2, "31": 2, "312": 2, "319": 2, "32": 2, "33": 2, "34": 2, "3477": 2, "3478": 2, "3492": 2, "3493": 2, "35": 2, "3509": 2, "3510": 2, "3525": 2, "3526": 2, "3545": 2, "3546": 2, "36": 2, "37": 2, "377684": 2, "38": 2, "382": 2, "383": 2, "384": 2, "385": 2, "386": 2, "387": 2, "388": 2, "389": 2, "39": 2, "390": 2, "395": 2, "396": 2, "397": 2, "4": 2, "40": 2, "402": 2, "403": 2, "408": 2, "409": 2, "4096": 2, "41": 2, "42": 2, "420": 2, "43": 2, "437": 2, "44": 2, "448": 2, "45": 2, "47": 2, "48": 2, "486": 2, "487": 2, "49": 2, "494": 2, "495": 2, "496": 2, "497": 2, "498": 2, "499": 2, "499013": 2, "5": 2, "50": 2, "500": 2, "501": 2, "502": 2, "507": 2, "508": 2, "509": 2, "51": 2, "514": 2, "515": 2, "517": 2, "52": 2, "520": 2, "521": 2, "528": 2, "53": 2, "533": 2, "534": 2, "549": 2, "55": 2, "56": 2, "565": 2, "57": 2, "580": 2, "59": 2, "6": 2, "60": 2, "600": 2, "61": 2, "62": 2, "623": 2, "628": 2, "629": 2, "63": 2, "637": 2, "64": 2, "65": 2, "657": 2, "66": 2, "660": 2, "67": 2, "671": 2, "676": 2, "681": 2, "683": 2, "688": 2, "7": 2, "70": 2, "712": 2, "719": 2, "72": 2, "728": 2, "73": 2, "74": 2, "75": 2, "756": 2, "76": 2, "761": 2, "763": 2, "767783": 2, "769559": 2, "77": 2, "771": 2, "78": 2, "781": 2, "785602": 2, "788": 2, "79": 2, "795": 2, "797": 2, "8": 2, "80": 2, "81": 2, "813": 2, "819": 2, "81920": 2, "821": 2, "83": 2, "85": 2, "853": 2, "858": 2, "87": 2, "88": 2, "89": 2, "899": 2, "9": 2, "90": 2, "93": 2, "953859": 2, "956": 2, "96": 2, "961": 2, "964": 2, "97": 2, "98": 2, "99": 2, "999999": 2, "A": 2, "As": 2, "But": 2, "FOR": 2, "For": 2, "IN": 2, "If": 2, "In": 2, "It": 2, "No": 2, "OF": 2, "ON": 2, "ONE": 2, "Of": 2, "On": [0, 2], "Or": 0, "The": 2, "There": 2, "To": [0, 2], "_": 2, "_a": 2, "_ab": 2, "_b": 2, "_build": 2, "_c": 2, "_d": 2, "_dummy1": 2, "_dummy2": 2, "_e": 2, "_f": 2, "_f1": 2, "_f2": 2, "_f3": 2, "_f4": 2, "_foo": 2, "_g": 2, "_nine": 2, "_t": 2, "_tq": 2, "_twelv": 2, "_v": 2, "_x": 2, "_x0": 2, "_x01": 2, "_x1": 2, "_x10": 2, "_x2": 2, "_x3": 2, "_x4": 2, "_x5": 2, "_y": 2, "_z": 2, "a1": 2, "a2": 2, "a_": 2, "ab": 2, "ab_": 2, "abbrevi": 2, "abort": 2, "about": 2, "abs_tac": 2, "absrep": 2, "absreptyp": 2, "abstract": 2, "abstyp": 2, "acc": 2, "acc_": 2, "acc_e0": 2, "acc_i": 2, "acc_i0": 2, "accf": 2, "accf_monoton": 2, "accord": 2, "accumul": 2, "accumulate_twice1": 2, "accumulate_twice2": 2, "ack": 2, "ackermann": 2, "ad": 2, "add": 2, "adepth": 2, "adj": 2, "ads_and_or": 2, "ads_or_and": 2, "after": 2, "al": 2, "all": 2, "all_equals_list": 2, "alon": 2, "alreadi": 2, "also": 2, "altern": 2, "an": [0, 2], "analysi": 2, "analyz": 2, "and_": 2, "and_associ": 2, "and_commut": 2, "and_ff": 2, "and_idempot": 2, "and_monoton": 2, "and_or": 2, "and_tt": 2, "andl": 2, "andr": 2, "ani": [0, 2], "answer": 2, "app": 2, "appear": 2, "append": 2, "appl": 2, "appli": 2, "applic": 2, "apply_2": 2, "apply_last": 2, "applyth": 2, "appuvar": 2, "apredf": 2, "apt": 0, "ar": [0, 2], "arg": 2, "argument": 2, "arithmet": 2, "ariti": 2, "around": 2, "arr": 2, "as_1": 2, "as_2": 2, "as_3": 2, "asclaus": 2, "ask": 2, "assert": 2, "assoc": 2, "associ": 2, "assum": 2, "assumpt": 2, "ast": 2, "atisym": 2, "atm": 2, "atom": 2, "auto": 2, "auto_monoton": 2, "autom": 2, "automat": 2, "aux": 2, "avail": 2, "avoid": 2, "axiom": 2, "axiomat": 2, "b": 2, "b1": 2, "b2": 2, "b2n": 2, "b_": 2, "backchain": 2, "backtrack": 2, "bad": 2, "bam": 2, "bang": 2, "bar": 2, "base": [0, 2], "basic": 2, "baz": 2, "bdepth": 2, "becasus": 2, "becaus": 2, "becom": 2, "befor": [0, 2], "belong": 2, "below": 2, "beta": 2, "beta_expand": 2, "better": 2, "between": 2, "bi": 2, "bidirect": 2, "bind": 2, "bit": 2, "block": 2, "bo": 2, "bodi": 2, "bool": 2, "bool2": 2, "both": [0, 2], "both_or_non": 2, "bound": 2, "box": 2, "brain": 2, "branch": 2, "broken": 2, "btl": 2, "btw": 2, "bug": 2, "build": 2, "build_pred": 2, "build_quantified_pred": 2, "built": 2, "builtin": 2, "c": 2, "c0": 2, "c1": 2, "c2": 2, "c3": 2, "c4": 2, "c5": 2, "c6": 2, "call": 2, "callback_prov": 2, "can": [0, 2], "cannot": 2, "canon": 2, "canonicaltac": 2, "captur": 2, "cardin": 2, "cartesian": 2, "case": 2, "case_disj_union": 2, "case_disj_union_inj1": 2, "case_disj_union_inj2": 2, "case_univ": 2, "case_univ_inj1": 2, "case_univ_inj2": 2, "cast": 2, "cbn": 2, "cbv": 2, "cd": 2, "cert": 2, "certif": 2, "chang": 2, "charact": 2, "check": 2, "check1": 2, "check1axm": 2, "check1decl": 2, "check1def": 2, "check1nbt": 2, "check1thm": 2, "check_codomain": 2, "check_domain": 2, "check_hyp": 2, "check_term": 2, "choic": 2, "choos": 2, "chr": 2, "chr_nokei": 2, "chr_nokey2": 2, "chr_not_cliqu": 2, "chr_sem": 2, "chrgcd": 2, "chrleq": 2, "classic": 2, "claus": 2, "clause1": 2, "clause2": 2, "clause3": 2, "close": 2, "cmp_term": 2, "code": 2, "column": 2, "come": 0, "comma": 2, "command": 2, "comment": 2, "common": 2, "commun": 0, "compat": 2, "compil": 2, "complet": 2, "con": 2, "concat1": 2, "confus": 2, "conj": 2, "conj2": 2, "conjunct": 2, "connect": 2, "consequ": 2, "consist": 2, "consol": 2, "const": 2, "constant": 2, "constant_tacl": 2, "constraint": 2, "cont": 2, "contain": 2, "content": 2, "context": 2, "contnext": 2, "conv": 2, "convention": 2, "converion": 2, "convers": 2, "copi": 2, "coq": 0, "correctli": 2, "could": 2, "counter": 2, "creat": [0, 2], "cross": 0, "cs_": 2, "cscript": 2, "ct": 2, "ctx": 2, "ctx_load": 2, "ctxconstr": 2, "current": [0, 2], "cut": 2, "cut2": 2, "cut3": 2, "cut4": 2, "cut5": 2, "cut6": 2, "cutth": 2, "d": 2, "d1": 2, "d11": 2, "d2": 2, "d22": 2, "d3": 2, "d33": 2, "d_": 2, "daemon": 2, "damag": 2, "data": 2, "dd": 2, "deal": 2, "debian": 0, "debprint": 2, "debug": 2, "debuggin": 2, "decis": 2, "decl": 2, "declar": 2, "declare_constraint": 2, "deep_index": 2, "def": 2, "def0": 2, "default": 2, "defin": 2, "definit": 2, "deftac": 2, "deftacl": 2, "delai": 2, "delay_outside_frag": 2, "denot": 2, "depend": 2, "deprec": 2, "depth": 2, "depth_tac": 2, "desper": 2, "desperate2": 2, "desperate3": 2, "develop": 2, "diagnost": 2, "did": 2, "differ": 2, "direct": 2, "directli": 0, "directori": 0, "dirti": 2, "discard": 2, "discuss": 2, "disj": 2, "disj_union": 2, "disjoint": 2, "distinct": 2, "distinct_nam": 2, "distrib": 0, "div": 2, "diverg": 2, "do": 2, "doc": [0, 2], "document": [0, 2], "doe": 2, "doesn": 2, "done": 2, "doom": 2, "doubl": 2, "down": 2, "drop": 2, "due": 2, "dummi": 2, "dummy1": 2, "dummy1_": 2, "dummy2": 2, "dummy2_": 2, "dune": 2, "duplic": 2, "e": [0, 2], "e1": 2, "e2": 2, "e_": 2, "eager": 2, "echo": 2, "effici": 2, "eg": 2, "either": 0, "eject_inject_limit_univ": 2, "eject_limit_univ": 2, "ejection_injection_univ": 2, "ejection_univ": 2, "element": 2, "elimin": 2, "elimthm": 2, "elp": 2, "elpi": 2, "elpi_api": 2, "elpi_only_llam": 2, "els": 2, "empti": 2, "en": 0, "end": 2, "end_com": 2, "end_of_proof": 2, "engin": 2, "enrico": 2, "enter": 2, "env": 2, "eq": 2, "eq_reflex": 2, "eq_to_impl": 2, "eq_to_impl_b": 2, "eq_to_impl_f": 2, "eq_true_intro": 2, "equal": 2, "equival": 2, "erro": 2, "error": 2, "escap": 2, "eta": 2, "eta_a": 2, "eval": 2, "evalu": 2, "even": 2, "everyth": 2, "exampl": 2, "except": 2, "exec": 2, "exist": 2, "existence_condit": 2, "exists_": 2, "exists_i": 2, "exists_monoton": 2, "exit": 2, "exp": 2, "expand": 2, "expect": 2, "explicitli": 0, "export": 2, "ext": 0, "extend": 2, "extern": 0, "extra": 2, "f": 2, "f1": 2, "f1_": 2, "f2": 2, "f2_": 2, "f3": 2, "f3_": 2, "f4": 2, "f4_": 2, "f_": 2, "facil": 2, "fail": 2, "failur": 2, "fallback": 0, "fals": 2, "famili": 2, "fatal": 2, "ff": 2, "ff_elim": 2, "file": [0, 2], "filter": 2, "find": 2, "findal": 2, "first": 2, "first_claus": 2, "five": 2, "fix": 2, "fixdef": 2, "fixiti": 2, "fixpoint": 2, "fixpoint_is_fixpoint": 2, "fixpoint_is_prefixpoint": 2, "fixpoint_subseteq_any_fixpoint": 2, "fixpoint_subseteq_any_prefixpoint": 2, "flat": 2, "flexibl": 2, "flush": 2, "fn": 2, "focus": 2, "fold": 2, "fold2_append": 2, "follow": [0, 2], "foo": 2, "foo1": 2, "foo2": 2, "foo3": 2, "foo4": 2, "foral": 2, "forall_": 2, "forall_i": 2, "forall_monoton": 2, "forc": 2, "form": 2, "formal": 2, "formed": 2, "formula": 2, "found": 2, "four": 2, "fp": 2, "fr": 0, "fragil": 2, "fragment": 2, "fragment_exit": 2, "fragment_exit2": 2, "fragment_exit3": 2, "free": 2, "fresh": 2, "fresh_": 2, "from": 2, "front": 2, "frozen": 2, "fst": 2, "ft": 2, "fun": 2, "function": 2, "funnam": 2, "g": [0, 2], "g1": 2, "g2": 2, "g_": 2, "gamma": 2, "gamma1": 2, "gamma2": 2, "gc": 2, "gcd": 2, "gener": [0, 2], "general_cas": 2, "general_case2": 2, "general_case3": 2, "get": 2, "gettimeofdai": 2, "github": 0, "githubpag": 0, "global": 2, "go": 2, "goal": 2, "goaltact": 2, "group": 2, "gx": 2, "gy": 2, "h": 2, "h1": 2, "h2": 2, "ha": 2, "hack": 2, "halt": 2, "hand": 2, "handl": 2, "happen": 2, "hard": 2, "hash": 2, "hashtbl": 2, "have": [0, 2], "hc_interp": 2, "hd": 2, "hdclaus": 2, "he": 2, "head": 2, "heap_discard": 2, "helper": 0, "henc": 2, "here": 2, "higher": 2, "hindlei": 2, "ho": 2, "hoc": 2, "hol": 2, "hollight": 2, "hollight_legaci": 2, "home": 2, "hook": 2, "horn": 2, "how": 2, "html": 0, "http": 0, "hurt": 2, "hyp": 2, "hyp_uvar": 2, "hypothes": 2, "hypothesi": 2, "hypsuchthat": 2, "i": [0, 2], "id": 2, "idempot": 2, "identifi": 2, "ig": 2, "ign": 2, "ignor": 2, "ih1": 2, "ih2": 2, "ii": 2, "illustr": 2, "immedi": 2, "imp": 2, "impl": 2, "impl2": 2, "impl_monoton": 2, "impl_not_not": 2, "implement": 2, "implic": 2, "implicit": 2, "in_subseteq": 2, "in_two": 2, "in_two_": 2, "in_two_e0": 2, "in_two_ff": 2, "in_two_i": 2, "in_two_tt": 2, "in_twof": 2, "in_twof_monoton": 2, "includ": 2, "incompat": 2, "increas": 2, "index": 2, "index2": 2, "induct": 2, "inductive_def": 2, "inductive_def_pkg": 2, "inductive_typ": 2, "ineffici": 2, "inequ": 2, "infer": 2, "infix": 2, "infixl": 2, "infixr": 2, "inj": 2, "inj1_disj_union": 2, "inj1_disj_union_inj": 2, "inj1_univ": 2, "inj1_univ_inj": 2, "inj2_disj_union": 2, "inj2_disj_union_inj": 2, "inj2_univ": 2, "inj2_univ_inj": 2, "inject": [0, 2], "inject_limit_univ": 2, "injection_univ": 2, "injection_univ_inj": 2, "input": 2, "inria": 0, "insid": 2, "inspect": 2, "instal": [0, 2], "instead": [0, 2], "int": 2, "int_tac": 2, "integ": 2, "inter": 2, "interact": 2, "interactive_tac": 2, "interest": 2, "interfac": 2, "interpret": 2, "intersphinx": 0, "introspect": 0, "introthm": 2, "inv": 2, "io_colon": 2, "is_fixpoint": 2, "is_ground": 2, "is_nat": 2, "is_nat_": 2, "is_nat_e0": 2, "is_nat_i": 2, "is_nat_monoton": 2, "is_nat_z": 2, "is_natf": 2, "is_pair": 2, "is_subset": 2, "is_subset_": 2, "itac": 2, "itaut": 2, "itauteq": 2, "iter": 2, "its": [0, 2], "j": 2, "just": 2, "jwintz": 2, "k": 2, "k1": 2, "k2": 2, "kernel": 2, "keyword": 2, "kill": 2, "kind": 2, "knaster": 2, "known": 2, "ko": 2, "ko1": 2, "ko2": 2, "l": 2, "l1": 2, "l2": 2, "lam": 2, "lambda": 2, "lambda2": 2, "lambda3": 2, "lambdaprolog": 2, "land_tac": 2, "langag": 2, "lappli": 2, "lapply_last": 2, "last": 2, "lazi": 2, "leancop": 2, "least": 2, "left": 2, "legaci": 1, "lemma": 2, "len": 2, "length": 2, "leq": 2, "less": 2, "let": 2, "level": 2, "lforal": 2, "lforall_last": 2, "lib": 2, "librari": 2, "light": 2, "like": 2, "line": 2, "linear": 2, "link": 0, "list": 2, "list_as_conj": 2, "list_comma": 2, "list_iter_rev": 2, "list_map": 2, "liter": 2, "literalinclud": 2, "llam": 2, "llamchr": 2, "local": 2, "logic": 2, "long": 2, "longer": 2, "look": 2, "loop": 2, "lost": 2, "lower": 2, "lprolog": 2, "lstop": 2, "lt": 2, "ltn": 2, "lvl": 2, "lx": 2, "ly": 2, "m": 2, "m1": 2, "m2": 2, "macro": 2, "mai": 2, "main": 2, "main1": 2, "main2": 2, "make": [0, 2], "makefil": 0, "man": 2, "manag": 0, "mani": 2, "map": 2, "map_list": 2, "map_list_opt": 2, "mark": 2, "master": 0, "match": 0, "matter": 2, "mayb": 2, "mean": 2, "meant": 0, "mem": 2, "mem_": 2, "memb": 2, "merg": 2, "mess": 2, "messag": 2, "meta": 2, "metavari": 2, "milner": 2, "miss": 2, "mistak": 2, "mixfix": 2, "mk": 2, "mk_bounded_fresh": 2, "mk_constant_list": 2, "mk_intro_thm": 2, "mk_list_of_bounded_fresh": 2, "mk_script": 2, "ml": 2, "mod": 2, "mode": 2, "modifi": 2, "modul": [0, 2], "mono": 2, "monoton": 2, "monthm": 2, "more": 2, "move": 2, "mp": 2, "much": 2, "mult": 2, "must": 2, "myabs2": 2, "myabsrep2": 2, "mybool2_": 2, "myformula": 2, "mynot": 2, "mynot_mynot_mytt": 2, "mynot_transf": 2, "myprop": 2, "myproprep2": 2, "myrep2": 2, "myrepabs2": 2, "mytt": 2, "mytt_transf": 2, "n": 2, "n1": 2, "n2": 2, "name": [0, 2], "name1": 2, "name_builtin": 2, "named_clauses00": 2, "named_clauses01": 2, "named_clauses02": 2, "namespac": 2, "namespaces00": 2, "namespaces01": 2, "namespaces02": 2, "namespaces03": 2, "nat": 2, "nat_": 2, "nat_ab": 2, "nat_abs_inj": 2, "nat_absrep": 2, "nat_cas": 2, "nat_case_": 2, "nat_case_z": 2, "nat_proprep": 2, "nat_rec": 2, "nat_rec_ok": 2, "nat_rec_ok0": 2, "nat_recf": 2, "nat_rep": 2, "nat_rep_inj": 2, "nat_repab": 2, "natur": 2, "need": 2, "neq": 2, "never": 2, "new": 2, "new2": 2, "new_basic_typ": 2, "new_certif": 2, "new_interactive_tac": 2, "new_tac": 2, "newcom": 2, "newl": 2, "newlazi": 2, "newt": 2, "next": 2, "next_object": 2, "next_tact": 2, "next_tactic0": 2, "nil": 2, "nil_con": 2, "nine": 2, "nine_": 2, "no_more_ch": 2, "nojekyl": 0, "non": 2, "non_interactive_tac": 2, "normal": 2, "not_": 2, "not_and": 2, "not_attack": 2, "not_attack_aux": 2, "not_defin": 2, "not_eq_inj1_inj2_univ": 2, "not_equal_z_": 2, "not_i": 2, "not_monoton": 2, "not_not_not": 2, "not_or": 2, "notat": 2, "notation_error": 2, "notation_legaci": 2, "note": 2, "noth": 2, "now": 2, "nr": 2, "num": 2, "number": 2, "o": 2, "object": [0, 2], "ocaml": 2, "ocamlc": 2, "ocamlopt": 2, "occur": 2, "occurr": 2, "odd": 2, "og": 2, "oh1": 2, "oh2": 2, "ok": 2, "old": 2, "omit": 2, "onc": 2, "one": [0, 2], "ones": 2, "onli": 2, "opam": 2, "oper": 2, "opr": 2, "optim": 2, "option": [1, 2], "or_": 2, "or_and": 2, "or_associ": 2, "or_commut": 2, "or_ff": 2, "or_idempot": 2, "or_monoton": 2, "or_tt": 2, "order": 2, "orels": 2, "org": 0, "origti": 2, "orl": 2, "orr": 2, "otac": 2, "other": [0, 2], "other_tac": 2, "otherwis": 2, "our": 2, "out": 2, "out1": 2, "outcom": 2, "output": 2, "outs2": 2, "outsid": 2, "over": 2, "overbar": 2, "own": 0, "p": 2, "p1": 2, "p2": 2, "p_tactic": 2, "pa": 2, "packag": [0, 2], "page": [0, 2], "pair": 2, "pair_univ": 2, "pair_univ_inj_l": 2, "pair_univ_inj_r": 2, "param": 2, "pars": 2, "parse_axiom": 2, "parse_def": 2, "parse_inductive_def_spec": 2, "parse_nbt": 2, "parse_obj": 2, "parse_thm": 2, "parser": [1, 2], "parsetac": 2, "parseterm": 2, "pass": 2, "path": 2, "pathfroma": 2, "pattern": 2, "patternunif": 2, "patternunif2": 2, "pb": 2, "pc": 2, "pcanonicaltac": 2, "pdef": 2, "perp": 2, "pf": 2, "pg": 2, "pgamma": 2, "pgoal": 2, "ph": 2, "pi": 2, "pi3": 2, "pi5": 2, "pip": 0, "pl": 2, "place": 0, "playground": 0, "pleas": 2, "plu": 2, "plugin": 0, "plus_": 2, "plus_comm": 2, "plus_n_": 2, "plus_n_z": 2, "plus_z": 2, "pnf": 2, "pnn": 2, "pnn_e": 2, "pnn_e0": 2, "pnn_has_two_valu": 2, "pnn_i": 2, "pnn_not": 2, "pnn_tt": 2, "pnnf": 2, "pnnf_monoton": 2, "point": 0, "poli": 2, "polymorph": 2, "polymorphic_vari": 2, "polyt": 2, "possibl": 2, "possibli": 2, "postfix": 2, "postfixl": 2, "pp": 2, "pp_tactic": 2, "ppp": 2, "ppptac": 2, "pptac": 2, "ppterm": 2, "pq": 2, "pr": 2, "preced": 2, "pred": 2, "pred_": 2, "pred_e0": 2, "pred_i": 2, "pred_well_found": 2, "predecessor": 2, "predf": 2, "predf_mon": 2, "predf_monoton": 2, "predic": 2, "prefix": 2, "prefixpoint_to_prefixpoint": 2, "prefixr": 2, "prenex": 2, "prep": 2, "preph": 2, "prephtyp": 2, "pretti": 2, "previou": 2, "primivit": 2, "principl": 2, "print": 2, "print_constraint": 2, "print_sequ": 2, "printer": 2, "probabl": 2, "problem": 2, "procedur": 2, "process_constructor": 2, "prod": 2, "prod_ab": 2, "prod_absrep": 2, "prod_proprep": 2, "prod_rep": 2, "prod_repab": 2, "produc": 2, "product": 2, "prog": 2, "program": 2, "progress": 2, "proj1_pair_univ": 2, "proj1_univ": 2, "proj2_pair_univ": 2, "proj2_univ": 2, "project": 0, "prolog": 2, "proof": 2, "prop": 2, "propag": 2, "properti": 2, "proposit": 2, "provabl": 2, "prove": 2, "prove_fix_elim_thm": 2, "prove_fix_intro_thm": 2, "prove_intro_thm": 2, "prove_monotonicity_thm": 2, "prover": 2, "provid": 2, "prune": 2, "prune_arg": 2, "prune_arg2": 2, "prune_arg3": 2, "pscript": 2, "pseq": 2, "pst": 2, "psttac": 2, "ptac": 2, "ptac1": 2, "ptac2": 2, "ptacl": 2, "ptacn": 2, "pty": 2, "ptybo": 2, "ptyp": 2, "ptype": 2, "publish": 0, "purpos": 2, "put": 2, "put_bind": 2, "px": 2, "py": 2, "python3": 0, "q": 2, "quant_fre": 2, "quantifi": 2, "quater": 2, "queen": 2, "queens_aux": 2, "queri": 2, "quote_syntax": 2, "r": 2, "r2": 2, "rand_tac": 2, "random": 2, "rang": 2, "rator_tac": 2, "re": 2, "reach": 2, "read": 2, "read_cmd": 2, "read_in_context": 2, "readterm": 2, "realiz": 2, "realli": 2, "rec": 2, "rec_is_fixpoint": 2, "recogn": 2, "recurs": 2, "reduc": 2, "reduce_cbn": 2, "reduce_cbv": 2, "reduct": 2, "ref": 2, "refer": [0, 2], "refl": 2, "refman": 0, "regress": 2, "relev": 2, "remain": 2, "remov": 2, "rep": 2, "repab": 2, "repabstyp": 2, "repeat": 2, "repres": 2, "reptyp": 2, "requir": 2, "resili": 2, "resolut": 0, "rest": 2, "restrict": 2, "restriction3": 2, "restriction4": 2, "restriction5": 2, "restriction6": 2, "restructuredtext": 2, "result": 2, "resumpt": 2, "reterm": 2, "retriev": 2, "return": 2, "rev": 2, "rev14": 2, "rid": 2, "right": 2, "ring": 2, "rl": 2, "robu": 2, "role": 0, "root": 0, "rtd": 0, "rule": 2, "run": 2, "runner": 2, "runtim": 2, "s1": 2, "s2": 2, "s_inj": 2, "safe_list_map": 2, "safeq": 2, "same": 2, "same_term": 2, "same_var": 2, "script": 2, "search": 2, "section": 0, "see": [0, 2], "seem": 2, "select": 2, "self": 0, "self_assign": 2, "self_init": 2, "semant": 2, "seq": 2, "sequent": 2, "set": 2, "shorten": 2, "shorten2": 2, "shorten_aux": 2, "shorten_aux2": 2, "shorten_builtin": 2, "shorten_tri": 2, "shot": 2, "shoud": 2, "should": 2, "sigma": 2, "silenc": 2, "simpl": 2, "simpli": 2, "sinc": 2, "singleton": 2, "six": 2, "size": 2, "skip": 2, "slow": 2, "small": 2, "snd": 2, "snippet": 2, "so": 2, "solv": 2, "some": 2, "sometim": 2, "somewher": 2, "sourc": [0, 2], "space": 2, "special": 2, "spent": 2, "sphinx": [0, 2], "spill_and": 2, "spill_impl": 2, "spill_lam": 2, "spy": 2, "src": 2, "src263": 2, "src265": 2, "st": 2, "stack": 0, "stai": 2, "standard": 2, "start": 2, "state": 2, "state_fixpoint_def": 2, "statement": 2, "statu": 2, "std": 2, "std_in": 2, "std_out": 2, "stderr": 2, "stdout": 2, "step0": 2, "step1": 2, "still": 2, "stm": 2, "stop": 2, "string": 2, "strip_const": 2, "structur": 2, "sttac": 2, "sub_tac": 2, "subformula": 2, "subproof": 2, "subset": 2, "subseteq": 2, "subst": 2, "substitut": 2, "succ": 2, "succe": 2, "success": 2, "successor": 2, "sum": 2, "super": 2, "support": 2, "sure": [0, 2], "suspend": 2, "sym": 2, "symbol": 2, "symptom": 2, "sync": 2, "system": 0, "t": 2, "t1": 2, "t1_": 2, "t2": 2, "t2_": 2, "t_": 2, "tabl": 2, "tac": 2, "tac1": 2, "tac2": 2, "tacl": 2, "tacn": 2, "tactic": 2, "target": 0, "tarski": 2, "tc": 2, "temporarili": 2, "ten": 2, "tenthousand": 2, "ter": 2, "term": 2, "termifi": 2, "termp": 2, "test1": 2, "test2": 2, "test3": 2, "test4": 2, "test5": 2, "test_appli": 2, "test_apply2": 2, "test_itaut_1": 2, "test_monotone1": 2, "test_monotone2": 2, "test_monotone3": 2, "text": 2, "teyju": 2, "tgt": 2, "th": 2, "than": 2, "the_librari": 2, "thei": 2, "them": 2, "theme": 0, "thenl": 2, "thenll": 2, "theorem": 2, "therefor": 2, "thi": [0, 2], "third": 2, "thm": 2, "thousand": 2, "three": 2, "through": 0, "time": 2, "time0": 2, "time1": 2, "time2": 2, "time_aft": 2, "tl": 2, "tl1": 2, "tm": 2, "tmp": 2, "todo": 2, "token": 2, "too": 2, "top": 2, "toplevel": 2, "toplevel_loop": 2, "toto": 2, "tp": 2, "trace": 2, "trace2": 2, "trace_chr": 2, "trace_cut": 2, "trace_findal": 2, "trail": 2, "tran": 2, "transfer": 2, "transform": 2, "tree": 0, "tri": 2, "trick": 2, "tricki": 2, "trigger": 2, "tru": 2, "true": 2, "true_then_fals": 2, "trust": 2, "try": 2, "try_claus": 2, "tt": 2, "tt_intro": 2, "ttl": 2, "turn": 2, "twelv": 2, "twelve_": 2, "two": 2, "tx": 2, "ty": 2, "tybo": 2, "tye": 2, "typ": 2, "typdef": 2, "type": 2, "typeabbrev": 2, "typeabbrv": 2, "typeabbrv1": 2, "typeabbrv10": 2, "typeabbrv11": 2, "typeabbrv12": 2, "typeabbrv2": 2, "typeabbrv3": 2, "typeabbrv4": 2, "typeabbrv5": 2, "typeabbrv6": 2, "typeabbrv7": 2, "typeabbrv8": 2, "typeabbrv9": 2, "typecheck": 2, "u": 2, "u1": 2, "u2": 2, "uid_priv": 2, "ulimit": 2, "ultim": 2, "uminu": 2, "unabl": 2, "unari": 2, "uncom": 2, "undeclar": 2, "unif": 2, "unif_1": 2, "unif_2": 2, "unif_zero": 2, "unifi": 2, "unimpl": 2, "union": 2, "univ": 2, "univers": 2, "unknown": 2, "unplacedq": 2, "unplacedqs1": 2, "unsaf": 2, "untrust": 2, "untyp": 2, "up": 2, "update_certif": 2, "us": [0, 2], "usag": 0, "user": 2, "usual": 2, "util": 2, "uu": 2, "uvar": 2, "uvar_1": 2, "uvar_2": 2, "uvar_3": 2, "uvar_4": 2, "uvar_5": 2, "uvar_6": 2, "uvar_chr": 2, "v": 2, "v1": 2, "v2": 2, "v_": 2, "valid": 2, "var": 2, "variabl": 2, "variad": 2, "variadic_declare_constraint": 2, "variant": 2, "veri": 2, "verifi": 2, "version": 2, "vg": 2, "via": 2, "vim": 2, "visual": 0, "vt": 2, "w": 2, "w_legaci": 2, "wa": 2, "wai": 2, "want": 2, "warn": 2, "watch": 2, "we": 2, "welcom": 2, "well": 2, "well_found": 2, "wgamma": 2, "what": 2, "whatev": 2, "when": 2, "where": 2, "which": [0, 2], "while": 2, "why": 2, "wit": 2, "within": 2, "without": 2, "wl": 2, "work": 2, "would": 2, "write": 2, "wrong": 2, "ww": 2, "www": 0, "x": 2, "x0": 2, "x01": 2, "x01_": 2, "x0_": 2, "x1": 2, "x10": 2, "x10_": 2, "x11": 2, "x12": 2, "x13": 2, "x14": 2, "x15": 2, "x16": 2, "x17": 2, "x18": 2, "x19": 2, "x1_": 2, "x2": 2, "x20": 2, "x21": 2, "x22": 2, "x23": 2, "x24": 2, "x25": 2, "x26": 2, "x2_": 2, "x3": 2, "x3_": 2, "x4": 2, "x4_": 2, "x5": 2, "x5_": 2, "x6": 2, "x7": 2, "x8": 2, "x9": 2, "x_": 2, "xa": 2, "xcon": 2, "xnil": 2, "xr": 2, "xt": 2, "xtac": 2, "xx": 2, "xxx": 2, "xxxxxxxxx": 2, "y": 2, "y2": 2, "y_": 2, "yap": 2, "yield": 2, "you": 2, "your": 2, "ysx": 2, "yx": 2, "yy": 2, "z": 2, "z_": 2, "zebra": 2, "zero": 2, "\u03bbprolog": 2}, "titles": ["About", "Welcome to Elpi\u2019s documentation!", "Playground"], "titleterms": {"": 1, "about": 0, "api": 1, "bed": 2, "build": 0, "document": 1, "elpi": 1, "extens": 0, "match": 2, "playground": 2, "prerequisit": [0, 2], "regexp": 2, "syntax": 2, "test": 2, "welcom": 1}})
\ No newline at end of file