blob: 1fd348f4ad47aca4b0d0ee3980e0546d7ca76e52 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>mathcomp.test_suite.hierarchy_test</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library mathcomp.test_suite.hierarchy_test</h1>
<div class="code">
</div>
<div class="doc">
Generated by etc/utils/hierarchy_test.py
</div>
<div class="code">
<br/>
</div>
<div class="doc">
`check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`.
</div>
<div class="code">
<span class="id" title="keyword">Tactic Notation</span> "check_join"<br/>
<span class="id" title="var">open_constr</span>(<span class="id" title="var">t1</span>) <span class="id" title="var">open_constr</span>(<span class="id" title="var">t2</span>) <span class="id" title="var">open_constr</span>(<span class="id" title="var">tjoin</span>) :=<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">T1</span> := <span class="id" title="var">open_constr</span>:(<span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <span class="id" title="var">t1</span>) <span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">T2</span> := <span class="id" title="var">open_constr</span>:(<span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <span class="id" title="var">t2</span>) <span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">match</span> <span class="id" title="var">tt</span> <span class="id" title="keyword">with</span><br/>
| <span class="id" title="var">_</span> ⇒ <span class="id" title="var">unify</span> ((<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <span class="id" title="var">t1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span>) <span class="id" title="var">T1</span>) ((<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <span class="id" title="var">t2</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span>) <span class="id" title="var">T2</span>)<br/>
| <span class="id" title="var">_</span> ⇒ <span class="id" title="tactic">fail</span> "There is no join of" <span class="id" title="var">t1</span> "and" <span class="id" title="var">t2</span><br/>
<span class="id" title="keyword">end</span>;<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">Tjoin</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="var">T1</span> <span class="id" title="keyword">with</span><br/>
| <span class="id" title="var">_</span> (<span class="id" title="var">_</span> ?<span class="id" title="var">Tjoin</span>) ⇒ <span class="id" title="keyword">constr</span>: (<span class="id" title="var">Tjoin</span>)<br/>
| <span class="id" title="var">_</span> ?<span class="id" title="var">Tjoin</span> ⇒ <span class="id" title="keyword">constr</span>: (<span class="id" title="var">Tjoin</span>)<br/>
| ?<span class="id" title="var">Tjoin</span> ⇒ <span class="id" title="keyword">constr</span>: (<span class="id" title="var">Tjoin</span>)<br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="tactic">in</span><br/>
<span class="id" title="var">is_evar</span> <span class="id" title="var">Tjoin</span>;<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">tjoin'</span> := <span class="id" title="keyword">type</span> <span class="id" title="keyword">of</span> <span class="id" title="var">Tjoin</span> <span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="var">tjoin'</span> <span class="id" title="keyword">with</span><br/>
| <span class="id" title="var">tjoin</span> ⇒ <span class="id" title="keyword">lazymatch</span> <span class="id" title="var">tjoin</span> <span class="id" title="keyword">with</span><br/>
| <span class="id" title="var">tjoin'</span> ⇒ <span class="id" title="tactic">idtac</span><br/>
| <span class="id" title="var">_</span> ⇒ <span class="id" title="tactic">idtac</span> <span class="id" title="var">tjoin'</span><br/>
<span class="id" title="keyword">end</span><br/>
| <span class="id" title="var">_</span> ⇒ <span class="id" title="tactic">fail</span> "The join of" <span class="id" title="var">t1</span> "and" <span class="id" title="var">t2</span> "is" <span class="id" title="var">tjoin'</span><br/>
"but is expected to be" <span class="id" title="var">tjoin</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Goal</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#False"><span class="id" title="inductive">False</span></a>.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
|
