File: BETA_TAC.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (26 lines) | stat: -rw-r--r-- 597 bytes parent folder | download | duplicates (11) 
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
 
\DOC BETA_TAC

\TYPE {BETA_TAC : tactic}

\SYNOPSIS
Beta-reduces all the beta-redexes in the conclusion of a goal.

\KEYWORDS
tactic.

\DESCRIBE
When applied to a goal {A ?- t}, the tactic {BETA_TAC} produces a new goal
which results from beta-reducing all beta-redexes, at any depth, in {t}.
Variables are renamed where necessary to avoid free variable capture.
{
    A ?- ...((\x. s1) s2)...
   ==========================  BETA_TAC
     A ?- ...(s1[s2/x])...
}
\FAILURE
Never fails, but will have no effect if there are no beta-redexes.

\SEEALSO
BETA_CONV, BETA_TAC, PAIRED_BETA_CONV.

\ENDDOC