diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.test_suite.hierarchy_test.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/mathcomp.test_suite.hierarchy_test.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.test_suite.hierarchy_test.html | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html b/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html new file mode 100644 index 0000000..1fd348f --- /dev/null +++ b/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html @@ -0,0 +1,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>
\ No newline at end of file |