@pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
(* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
@pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
(* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
:= mapOptionTreeAndFlatten (fun lt =>
match lt with t @@ l => match l with
| ec'::nil => if eqd_dec ec ec' then [t] else []
:= mapOptionTreeAndFlatten (fun lt =>
match lt with t @@ l => match l with
| ec'::nil => if eqd_dec ec ec' then [t] else []
(* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
(* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
(* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
(* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
(* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
(* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
: forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
| PCF_RArrange : ∀ x y t a, Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
| PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ ([],[_]) ] (RLit Γ Δ lit (ec::nil))
: forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
| PCF_RArrange : ∀ x y t a, Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
| PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ ([],[_]) ] (RLit Γ Δ lit (ec::nil))