name "apps_2_src" table { class "gray" [ { "component" * } { [ { "plane" * } { [ "files" * ] } ] } ] class "yellow" [ { "models" * } { [ { "term model" * } { [ "tm" * ] } ] [ { "denotational equivalence" * } { [ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ] } ] [ { "local environment interpretation" * } { [ "li" + "( ? ϵ ⟦?⟧{?}[?] )" "li_vpushs" * ] } ] [ { "multiple evaluation push" * } { [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpush_fold" * ] } ] [ { "evaluation equivalence" * } { [ "veq" + "( ? ≗{?} ? )" "veq_lifts" * ] } ] [ { "model declaration" * } { [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )" "model_vpush" + "( ⫯{?}[?←?]? )" "model_props" * ] } ] } ] (* class "yellow" [ { "MLTT1" * } { [ { "" * } { [ "genv_primitive" "judgment" * ] } ] } ] *) class "orange" [ { "functional" * } { [ { "multiple filling" * } { [ "mf" + "( ●[?,?]? )" "mf_exeq" "mf_lifts" "mf_cpr" *] [ "mf_vpush" + "( ⇡[?←?]? )" "mf_vpush_exteq" "mf_vpush_vlift" * ] [ "mf_vlift" + "( ⇡[?]? )" "mf_vlift_exteq" * ] [ "mf_v" * ] } ] [ { "relocation" * } { [ "flifts_basic" + "( ↑[?,?]? )" "flifts_flifts_basic" * ] [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )" "flifts_flifts" * ] } ] } ] class "red" [ { "examples" * } { [ { "terms with special features" * } { [ (* "ex_sta_ldec" + *) "ex_cpr_omega" (* + "ex_fpbg_refl" + "ex_snv_eta" *) * ] } ] } ] } class "top" { * } class "capitalize italic" { 0 } class "italic" { 1 } (* [ { "evaluation drop" * } { [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ] } ] [ { "reduction and type machine" * } { [ "rtm" "rtm_step ( ? ⇨ ? )" * ] } ] *)