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
|
\DOC basic_convs
\TYPE {basic_convs : unit -> (string * (term * conv)) list}
\SYNOPSIS
List the current default conversions used in rewriting and simplification.
\DESCRIBE
The HOL Light rewriter ({REWRITE_TAC} etc.) and simplifier ({SIMP_TAC} etc.)
have default sets of (conditional) equations and other conversions that are
applied by default, except in the {PURE_} variants. A call to {basic_convs()}
returns the current set of conversions.
\FAILURE
Never fails.
\EXAMPLE
In the default HOL Light state the only conversions are for generalized beta
reduction and the reduction of pattern-matching constructs such as
{match...with}. All the other default simplifications are done by rewrite
rules.
{
# basic_convs();;
val it : (string * (term * conv)) list =
[("FUN_ONEPATTERN_CONV", (`_FUNCTION (\y z. P y z) x`, <fun>));
("MATCH_ONEPATTERN_CONV", (`_MATCH x (\y z. P y z)`, <fun>));
("FUN_SEQPATTERN_CONV", (`_FUNCTION (_SEQPATTERN r s) x`, <fun>));
("MATCH_SEQPATTERN_CONV", (`_MATCH x (_SEQPATTERN r s)`, <fun>));
("GEN_BETA_CONV", (`GABS (\a. b) c`, <fun>))]
}
\SEEALSO
basic_rewrites, extend_basic_convs, set_basic_convs.
\ENDDOC
|
