More about parsing

Consider the development about parsing well parenthetized strings (see here). Build a function with the following specification:

Definition parse_nest :
 forall l: list par,
  {l'':list par &
   {t:bin | parse_rel l l'' t}}+{forall l'' t', ~parse_rel l l'' t'}.

Solution

Last modified: Tue May 20 15:26:16 MEST 2003