Functions defined by cases without match
Consider the following type definition for vehicles (including bicycles
and motorized vehicles). For bicycles, we can have a variable number
of seats and for motorized vehicles we can have a variable number
of seats and a variable number of wheels:
Inductive vehicle : Set :=
| bicycle : nat -> vehicle
| motorized : nat -> nat -> vehicle.
Define a function computing the number of seats of any vehicle,
as an application of vehicle_rec (without using match ... with ).
Solution
This file