diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.test_suite.hierarchy_test.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
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, 0 insertions, 76 deletions
diff --git a/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html b/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html deleted file mode 100644 index 1fd348f..0000000 --- a/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html +++ /dev/null @@ -1,76 +0,0 @@ -<!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 |