fact: Fixpoint nom_interp (n:nat) (e:n_exp) (rho: nom_env) : res nom_val := match n with | 0 => timeout _ | S m => match e with | n_var x => match (rho_lookup x rho) with | Some (e',r') => nom_interp m e' r' | None => stuck _ end | n_app e1 e2 => match nom_interp m e1 rho with | val _ (nom_closure x rho' e1') => nom_interp m e1' (nom_cons x e2 rho rho') | r => r end | n_abs x e => val _ (nom_closure x rho e) end end.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas