-
- Definition count (n:nat) := count' n nil.
-
- Definition rebundle {Γ}(X:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) : list (HaskType Γ ★ ) :=
- map (fun n => fun TV ite => grab n (X TV ite)) (count (length (X _ (ite_unit _)))).
-
- Definition take_arg_types_as_tree Γ (ht:HaskType Γ ★) :=
- (unleaves' (rebundle (fun TV ite => (take_arg_types (ht TV ite))))).
+
+ Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
+ unleaves
+ (take_trustme
+ (count_arg_types (ht _ (ite_unit _)))
+ (fun TV ite => take_arg_types (ht TV ite))).