Subversion Repositories wimsdev

Rev

Rev 2071 | Rev 7210 | Go to most recent revision | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev Author Line No. Line
2071 zjchen 1 
!set methtit=删除无用的假设
2 
!set methparmtype=special
3 
!set methparmrelax=1
4 
!set stepnocount=yes
5 
!set methhelp=你可以用这个方法删除无用的假设,\
6 
 以净化环境. 不过, <b>请注意</b>! 如果你删除了必要的假设,\
7 
你将无法完成证明!\
8 
 <p>\
9 
任何时候你都可以使用这个方法而不用担心被扣分,\
10 
因为这不会增加推导的步数.
11 
!set N_=!linecnt $m_context
12 
 
13 
!if $wims_read_parm iswordof form check
14 
 !goto $wims_read_parm
15 
!endif
16 
 
17 
!if $N_<1
18 
 !set error1=目前情况下已经没有任何假设!
19 
!endif
20 
 
21 
!exit
22 
:form
23 
 $methhelp
24 
 <p>
25 
 这里是当前的假设. 标记你想删除的假设. <ul>
26 
 !for i=1 to $N_
27 
  !set l=!line $i of $m_context
5763 bpr 28 
  <li> <input type=checkbox name=methparm1 value=$i/> \($l)
2071 zjchen 29 
 !next i
30 
 </ul>
31 
!exit
32 
:check
33 
 !reset newobject,oldobject
34 
 n_=!itemcnt $methparm1
35 
 !if $n_=0
36 
  methexp=空的步骤
37 
  !exit
38 
 !endif
39 
 nc=
40 
 !for i=1 to $N_
41 
  !if $i notitemof $methparm1
42 
   l=!line $i of $m_context
43 
   nc=!append line $l to $nc
44 
  !endif
45 
 !next i
46 
 m_context=$nc
47 
 !read deduc/objects.combine
48 
 methexp=删除 $n_ hypotheses
49 
 
50 
!exit
51