3 <style type="text/css">
4 ul.spaced li { padding-bottom: 1em; }
5 ul.empty li { list-style-type: none; }
6 tt { font-weight: bold; background-color: lightgray; }
7 tt.uri { font-weight: normal; background-color: transparent; }
14 <img align="center" src="http://helm.cs.unibo.it/whelp.png" alt="whelp" />
19 <h2>Whelp Input Syntax</h2>
22 <b>locate <em><pattern></em></b>
24 <em><pattern></em> is a shell like pattern which could
25 include <tt>*</tt> (denoting any sequence of 0 or more characters)
26 and <tt>?</tt> (denoting any single character).<br />
31 <li> <tt>nat</tt> pattern matches
32 <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> only
34 <li> <tt>n?t</tt> pattern matches
35 <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> and
36 <tt class="uri">cic:/Coq/Init/Logic/not.con</tt>
38 <li> <tt>nat*</tt> pattern matches
39 <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt>,
40 <tt class="uri">cic:/Coq/Init/Peano/nat_case.con</tt> and many more
46 <b>match <em><term></em></b>
50 <li> <tt>\forall x,y:nat.x+y=y+x</tt>
51 (commutativity of natural plus)
53 <li> <tt>\forall x,y,z:R.x*(y+z)=x*y+x*z</tt>
54 (distributivity of real times over real plus)
56 <li> <tt>nat \to nat \to nat</tt>
57 (all binary functions over naturals)
63 <b>hint <em><term></em></b>
67 <li> <tt>\forall n:nat. (fact n) = n * (fact (n - 1))</tt>
68 (how could we prove <em>n! = (n-1)! * n</em> ?)
70 <li> <tt>\forall n:nat.n \lt n+5</tt>
71 (how could we prove <em>n < n + 5</em> ?)
73 <li> <tt>\forall x,y:nat. x*y \lt (S x)*(S y)</tt>
74 (how could we prove <em>x*y < (x+1)*(y+1)</em> ?)
80 <b>elim <em><identifier></em></b>
85 (induction/elimination principles over natural numbers)
88 (induction/elimination principles over lists)