[\lambda\delta home]
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
[Spacer]

home news specification

documentation implementation
foreword milestones version 2 (background - syntax - core - applications)
version 2 helena Open Symbolic Notation (OSN)
citations visibility version 1 (background - core) (static HELM directory) version 1 library (static LDDL directory)
Contents of the Specification [butterfly]
This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below.
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline.
category units




sizes characters (files) 24567 (42) nodes (objects) 94309 (139) intrinsic loss factor 3.8
propositions theorems 14 lemmas 84 total 98
concepts declared 6 defined 27 total 33
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
component plane files


models term model tm tm_vpush


denotational equivalence deq ( ? ⊢ ? ≗{?} ? ) deq_cpr


local environment interpretation li ( ? ϵ ⟦?⟧{?}[?] ) li_vpushs


multiple evaluation push vpushs ( ?⨁{?}[?]? ≘ ? ) vpushs_fold


evaluation equivalence veq ( ? ≗{?} ? ) veq_lifts


model declaration model ( ? ≗{?} ? ) ( ? @{?} ? ) ( ⟦?⟧{?}[?,?] ) model_vpush ( ⫯{?}[?←?]? ) model_props
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

examples terms with special features ex_cpr_omega ex_fpbg_refl ex_cnv_eta


[Spacer]

[Valid XHTML 1.1] [Valid CSS level 2] [Generated from XML via XSL] [PNG used here] [Viewable with any browser]

Last update: Thu, 08 Nov 2018 17:30:52 +0100