λδ digital library (LDDL)
home
news
specification
specification log
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
)
Constant
Definition:
imp
(
ld:
/
Environment
/
grundlagen_2
/
l
/
imp.ld
)
Informal description: ""
{
λ[a:
Prop
]
.
λ[b:
Prop
]
}
.
<
Prop
>
.
∀[x:
a
]
.
b
Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100