fact: Fixpoint decode (t : GenTree.tree nat) : option choice_type := match t with | GenTree.Leaf 1 => Some chUnit | GenTree.Leaf 2 => Some chBool | GenTree.Leaf 3 => Some chNat | GenTree.Leaf n => Some ( chFin (mkpos ((n - 4).+1)%N) ) | GenTree.Node 1 [:: l ; r] => match decode l, decode r with | Some l, Some r => Some (chProd l r) | _, _ => None end | GenTree.Node 2 [:: l ; r] => match decode l, decode r with | Some l, Some r => Some (chMap l r) | _, _ => None end | GenTree.Node 3 [:: l] => match decode l with | Some l => Some (chOption l) | _ => None end | _ => None end.
imports: Coq(Utf8 Lia) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples GenericRulesSimple) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr realsum seq all_algebra fintype) Crypt(Prelude Axioms) extructures(ord fset fmap) Mon(SPropBase) Equations(Equations)