---++ Syntax

<verbatim>
"if" Strategy "then" Strategy "end" -> Strategy
</verbatim>

---++ Description

The strategy
<verbatim>
if s1 then s2 end
</verbatim>

applies =s2= if =s1= succeeds. The result of =s1= is ignored. That is, if the condition

<verbatim>
<s1> t
</verbatim>

succeeds, then the result of

<verbatim>
<if s1 then s2 end> t
</verbatim>

is

<verbatim>
<s2> t
</verbatim>

On the other hand, if  the condition fails, then the result is =t=.

---++ Formatting

The if-then construct is usually formatted in the following way:

<verbatim>
if s1 then
  s2
end
</verbatim>

---++ Implementation

The if-then construct is sugar for a guarded left-choice. The strategy

<verbatim>
if s1 then s2 end
</verbatim>

translates into 

<verbatim>
where(s1) < s2 + id
</verbatim>