Section experiment Inductive state Type s1 state s2 state Fixpoint tra

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
Section experiment.
Inductive state : Type :=
| s1 : state
| s2 : state.
Fixpoint transitions(s:state):state :=
match s with
| s1 => s2
| s2 => s2
end.
Eval compute in (transitions s1).
Example test_transitions:
(transitions (transitions s1)) = s2.
Proof. simpl. reflexivity. Qed.
End experiment.