- Moogle Input Syntax
+ Whelp Input Syntax
-
locate <pattern>
@@ -27,27 +29,66 @@
Examples:
- nat pattern matches
- cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) only
+ cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) only
- n?t pattern matches
- cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) and
- cic:/Coq/Init/Logic/not.con
+ cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) and
+ cic:/Coq/Init/Logic/not.con
- nat* pattern matches
- cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1),
- cic:/Coq/Init/Peano/nat_case.con and many more
+ cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1),
+ cic:/Coq/Init/Peano/nat_case.con and many more
-
- hint
+ match <term>
+
+ Examples:
+
+ - \forall x,y:nat.x+y=y+x
+ (commutativity of natural plus)
+
+ - \forall x,y,z:R.x*(y+z)=x*y+x*z
+ (distributivity of real times over real plus)
+
+ - nat \to nat \to nat
+ (all binary functions over naturals)
+
+
+
-
- match
+ hint <term>
+
+ Examples:
+
+ - \forall n:nat. (fact n) = n * (fact (n - 1))
+ (how could we prove n! = (n-1)! * n ?)
+
+ - \forall n:nat.n \lt n+5
+ (how could we prove n < n + 5 ?)
+
+ - \forall x,y:nat. x*y \lt (S x)*(S y)
+ (how could we prove x*y < (x+1)*(y+1) ?)
+
+
+
-
- elim
+ elim <identifier>
+
+ Examples:
+
+ - nat
+ (induction/elimination principles over natural numbers)
+
+ - list
+ (induction/elimination principles over lists)
+
+
+
|