fact: Fixpoint print_clos c := match c with | Closed t e => (print_term t ++ "↓" ++ print_env e)%string | Cont s => "k[" ++ print_stack s ++ "]" end with print_stack s := match s with | Scst α => print_sconst α | Scons c s' => print_clos c ++ "°" ++ print_stack s' end with print_env e := match e with | Enil => "∅"%string | Econs n c Enil => n ++ " ↦ " ++ print_clos c | Econs n c e' => n ++ " ↦ " ++ print_clos c ++ ", " ++ print_env e' end.
imports: Bool String Coq.Classes.RelationClasses