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
|
\section{Error messages}
\index{errors!illegal pattern construction}
This session illustrates some of the top-level error messages caused by using
an illegal pattern constructor within a side-condition.
\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
_ _ __ _ __ __
|___ |__| | | | |__| |__|
| | | |__| |__ |__| |__|
Version 2
#load_library `trs`;;
Loading library `trs` ...
Updating help search path
.............................................................................
......................
Library `trs` loaded.
() : void
#find_theorems ((conc "x:bool") Where (kind Axiom))
# (Paths [Theory `arithmetic`]);;
evaluation failed Where -- `Kind' used in side-condition
#find_theorems ((conc "x:bool") Where (conc "a * b"))
# (Paths [Theory `arithmetic`]);;
evaluation failed Where -- `Conc' used in side-condition
#find_theorems ((conc "x:bool")
# Where (("x:bool" contains "a * b")
# Where ("a:num" contains "l - m")))
# (Paths [Theory `arithmetic`]);;
evaluation failed Where -- `Where' used in side-condition
#find_theorems (((conc "x:bool") Where ("x:bool" contains "a * b"))
# Where ("a:num" contains "l - m"))
# (Paths [Theory `arithmetic`]);;
Searching theory arithmetic
Step([((Theorem),
`arithmetic`,
`RIGHT_SUB_DISTRIB`,
|- !m n p. (m - n) * p = (m * p) - (n * p))],
-)
: searchstep
#quit();;
$
\end{verbatim}\end{session}
|
