libaac-tactics-coq 0.2.pl2-4build1 / usr / share / doc / libaac-tactics-coq / api / type_AAC_matcher.html

This file is indexed.

/usr/share/doc/libaac-tactics-coq/api/type_AAC_matcher.html is in libaac-tactics-coq 0.2.pl2-4build1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
<html><head>
<link rel="stylesheet" href="style.css" type="text/css">
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
<link rel="Start" href="index.html">
<link title="Index of types" rel=Appendix href="index_types.html">
<link title="Index of values" rel=Appendix href="index_values.html">
<link title="Index of modules" rel=Appendix href="index_modules.html">
<link title="Index of module types" rel=Appendix href="index_module_types.html">
<link title="AAC_coq" rel="Chapter" href="AAC_coq.html">
<link title="AAC_helper" rel="Chapter" href="AAC_helper.html">
<link title="AAC_search_monad" rel="Chapter" href="AAC_search_monad.html">
<link title="AAC_matcher" rel="Chapter" href="AAC_matcher.html">
<link title="AAC_theory" rel="Chapter" href="AAC_theory.html">
<link title="AAC_print" rel="Chapter" href="AAC_print.html">
<link title="AAC_rewrite" rel="Chapter" href="AAC_rewrite.html"><title>AAC_matcher</title>
</head>
<body>
<code class="code"><span class="keyword">sig</span><br>
&nbsp;&nbsp;<span class="keyword">type</span>&nbsp;symbol&nbsp;=&nbsp;int<br>
&nbsp;&nbsp;<span class="keyword">type</span>&nbsp;var&nbsp;=&nbsp;int<br>
&nbsp;&nbsp;<span class="keyword">type</span>&nbsp;units&nbsp;=&nbsp;(<span class="constructor">AAC_matcher</span>.symbol&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.symbol)&nbsp;list<br>
&nbsp;&nbsp;<span class="keyword">type</span>&nbsp;ext_units&nbsp;=&nbsp;{<br>
&nbsp;&nbsp;&nbsp;&nbsp;unit_for&nbsp;:&nbsp;<span class="constructor">AAC_matcher</span>.units;<br>
&nbsp;&nbsp;&nbsp;&nbsp;is_ac&nbsp;:&nbsp;(<span class="constructor">AAC_matcher</span>.symbol&nbsp;*&nbsp;bool)&nbsp;list;<br>
&nbsp;&nbsp;}<br>
&nbsp;&nbsp;<span class="keyword">type</span>&nbsp;<span class="keywordsign">'</span>a&nbsp;mset&nbsp;=&nbsp;(<span class="keywordsign">'</span>a&nbsp;*&nbsp;int)&nbsp;list<br>
&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;linear&nbsp;:&nbsp;<span class="keywordsign">'</span>a&nbsp;<span class="constructor">AAC_matcher</span>.mset&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="keywordsign">'</span>a&nbsp;list<br>
&nbsp;&nbsp;<span class="keyword">module</span>&nbsp;<span class="constructor">Terms</span>&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">sig</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">type</span>&nbsp;t&nbsp;=<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">Dot</span>&nbsp;<span class="keyword">of</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="constructor">AAC_matcher</span>.symbol&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t)<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keywordsign">|</span>&nbsp;<span class="constructor">Plus</span>&nbsp;<span class="keyword">of</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="constructor">AAC_matcher</span>.symbol&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t)<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keywordsign">|</span>&nbsp;<span class="constructor">Sym</span>&nbsp;<span class="keyword">of</span>&nbsp;(<span class="constructor">AAC_matcher</span>.symbol&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;array)<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keywordsign">|</span>&nbsp;<span class="constructor">Var</span>&nbsp;<span class="keyword">of</span>&nbsp;<span class="constructor">AAC_matcher</span>.var<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keywordsign">|</span>&nbsp;<span class="constructor">Unit</span>&nbsp;<span class="keyword">of</span>&nbsp;<span class="constructor">AAC_matcher</span>.symbol<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;equal_aac&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.units&nbsp;<span class="keywordsign">-&gt;</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;bool<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">type</span>&nbsp;nf_term<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;nf_term_compare&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.nf_term&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.nf_term&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;int<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;nf_equal&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.nf_term&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.nf_term&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;bool<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;sprint_nf_term&nbsp;:&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.nf_term&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;string<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;term_of_t&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.units&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.nf_term<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;t_of_term&nbsp;:&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.nf_term&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t<br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">end</span><br>
&nbsp;&nbsp;<span class="keyword">module</span>&nbsp;<span class="constructor">Subst</span>&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">sig</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">type</span>&nbsp;t<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;sprint&nbsp;:&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Subst</span>.t&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;string<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;instantiate&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Subst</span>.t&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;to_list&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Subst</span>.t&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;(<span class="constructor">AAC_matcher</span>.var&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t)&nbsp;list<br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">end</span><br>
&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;matcher&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;?strict:bool&nbsp;<span class="keywordsign">-&gt;</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.ext_units&nbsp;<span class="keywordsign">-&gt;</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;<span class="keywordsign">-&gt;</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;<span class="keywordsign">-&gt;</span>&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Subst</span>.t&nbsp;<span class="constructor">AAC_search_monad</span>.m<br>
&nbsp;&nbsp;<span class="keyword">val</span>&nbsp;subterm&nbsp;:<br>
&nbsp;&nbsp;&nbsp;&nbsp;?strict:bool&nbsp;<span class="keywordsign">-&gt;</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.ext_units&nbsp;<span class="keywordsign">-&gt;</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;<span class="keywordsign">-&gt;</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;<span class="keywordsign">-&gt;</span><br>
&nbsp;&nbsp;&nbsp;&nbsp;(int&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Terms</span>.t&nbsp;*&nbsp;<span class="constructor">AAC_matcher</span>.<span class="constructor">Subst</span>.t&nbsp;<span class="constructor">AAC_search_monad</span>.m)<br>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="constructor">AAC_search_monad</span>.m<br>
<span class="keyword">end</span></code></body></html>

APT Browse - Built by Thomas Orozco.