data State = Idle | Waiting | Connected data Message = Hello Int | Data Int | Close match classify (s : State) (m : Message) : Int = | Idle (Hello n) -> n | Idle (Data n) -> n | Idle Close -> 0 | Waiting (Hello n) -> n | Waiting (Data n) -> n | Waiting Close -> 0 | Connected (Hello n) -> n | Connected (Data n) -> n | Connected Close -> 0