Inductive state Type s1 state s2 state Fixpoint transitions state stat

1
2
3
4
5
6
7
8
9
Inductive state : Type :=
| s1 : state
| s2 : state.
Fixpoint transitions(s:state):state :=
match s with
| s1 => s2
| s2 => s2
end.