fact: Definition machine_step (avoid : atoms) (c : configuration) : Step configuration := match c with (h, t, s) => if isVal t then match s with | nil => Done _ | n_app2 t2 :: s' => match t with | n_abs x t1 => if AtomSetProperties.In_dec x (dom h `union` avoid) then let (y,_) := atom_fresh (dom h `union` avoid) in TakeStep _ ((y,t2)::h, swap x y t1, s') else TakeStep _ ((x,t2)::h, t1, s') | _ => Error _ end end else match t with | n_var x => match get x h with | Some t1 => TakeStep _ (h, t1, s) | None => Error _ end | n_app t1 t2 => TakeStep _ (h, t1, n_app2 t2 :: s) | _ => Error _ end end.
imports: Lia Metalib.Metatheory Metalib.LibLNgen