[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	nat-set	f	nat-set → nat
# .	lp-array	f	lp-array → nat
# .	nat-list	f	nat-list → nat
. '	nat-list	f	nat → nat-list
. + .	nat-basic2	f	nat × nat → nat
. + .	nat-list	f	nat × nat-list → nat-list
. + .	nat-list	f	nat-list × nat → nat-list
. + .	nat-list	f	nat-list × nat-list → nat-list
. ++ .	nat-set	f	nat-set × nat → nat-set
. ++ .	nat-list	f	nat-list × nat → nat-list
. +@ .	nat-list	f	nat × nat → nat-list
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	nat-set	f	nat-set × nat → nat-set
. -1	nat-basic1	f	nat → nat
. -1@ .	nat-list	f	nat-list × nat → nat-list
. -1l .	nat-list	f	nat-list × nat → nat-list
. -l .	nat-list	f	nat-list × nat → nat-list
. .butlast	nat-list	f	nat-list → nat-list
. .butmax	nat-set	f	nat-set → nat-set
. .butmin	nat-set	f	nat-set → nat-set
. .filter ( . )	array-indices	f	nat-set × (nat → bool) → nat-set
. .first	nat-list	f	nat-list → nat
. .flags	lprops	f	lprops → lpropflags
. .flags:= .	lprops	f	lprops × lpropflags → lprops
. .gcheapidx	lprops	f	lprops → nat
. .gcheapidx:= .	lprops	f	lprops × nat → lprops
. .indicesWhere ( . )	lp-array	f	lp-array × (lprops → bool) × nat → nat-list
. .indicesWhere ( . )	lp-array	f	lp-array × (lprops → bool) → nat-list
. .last	nat-list	f	nat-list → nat
. .map ( . )	lp-array	f	lp-array × (lprops → lprops) → lp-array
. .map ( . )	array-indices	f	nat-set × (nat → nat) → nat-set
. .mapIf ( . )	lp-array	f	lp-array × (lprops → bool) × (lprops → lprops) × nat → lp-array
. .mapIf ( . )	lp-array	f	lp-array × (lprops → bool) × (lprops → lprops) → lp-array
. .mapIndices ( . )	lp-array	f	lp-array × nat-list × (lprops → lprops) → lp-array
. .mapIndices ( . )	lp-array	f	lp-array × nat-set × (lprops → lprops) → lp-array
. .max	nat-set	f	nat-set → nat
. .min	nat-set	f	nat-set → nat
. .ref-size	lprops	f	lprops → nat
. .ref-size:= .	lprops	f	lprops × nat → lprops
. .rest	nat-list	f	nat-list → nat-list
. .size	lprops	f	lprops → nat
. .size:= .	lprops	f	lprops × nat → lprops
. < .	nat-set	p	nat-set × nat
. < .	nat-set	p	nat × nat-set
. < .	nat-basic1	p	nat × nat
. < .	nat-list-less	p	nat-list × nat
. < .	nat-list	p	nat-list × nat-list
. > .	nat	p	nat × nat
. [ . ]	nat-list	f	nat-list × nat → nat
. [ . ]	nat-list	f	nat-list × nat × nat → nat-list
. [ . ]	lp-array	f	lp-array × nat → lprops
. [ . ]	lp-array	f	lp-array × nat × lprops → lp-array
. \ .	nat-set	f	nat-set × nat-set → nat-set
. ∈ .	nat-set	p	nat × nat-set
. ∈ .	lp-array	p	lprops × lp-array
. ∈ .	nat-list	p	nat × nat-list
. ∩ .	nat-set	f	nat-set × nat-set → nat-set
. ∪ .	nat-set	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	nat-set	p	nat-set × nat-set
. ⊑ .	nat-list	p	nat-list × nat-list
. ⊒ .	nat-list	p	nat-list × nat-list
[]	nat-list	c	nat-list
{ . }	nat-set	f	nat → nat-set
φ	lp-array	v	lprops → bool
φn	array-indices	v	nat → bool
∅	nat-set	c	nat-set
LP_FREE	lprops	c	lpropflags
LP_GROUP_NODES	lprops	c	lpropflags
LP_INDEX_NODES	lprops	c	lpropflags
butlastn	nat-list	f	nat × nat-list → nat-list
cmp	lp-array	p	lp-array × lprops × nat × nat
cmp	lp-array	p	lp-array × nat × lp-array × nat × nat
copy	lp-array	f	lp-array × nat × lp-array × nat × nat → lp-array
disj	nat-list	p	nat-list × nat-list
dups	nat-list	p	nat-list
fill	lp-array	f	lp-array × lprops × nat × nat → lp-array
fill	lp-array	f	lp-array × lprops → lp-array
fillfirst	nat-list	f	nat × nat × nat-list → nat-list
firstn	nat-list	f	nat × nat-list → nat-list
fn	array-indices	v	nat → nat
frome	nat-list	f	nat-list × nat → nat-list
id○	lp-array	p	lp-array × lp-array × nat
idrange	lp-array	p	lp-array × nat × nat
lastn	nat-list	f	nat × nat-list → nat-list
lp	lprops	v	lprops
lp-array	lp-array	s
lp0	lprops	v	lprops
lp1	lp-array	v	lprops
lpf	lprops	v	lpropflags
lpf0	lprops	v	lpropflags
lpropflags	lprops	s
lprops	lprops	s
lpt	lp-array	v	lp-array
lpt0	lp-array	v	lp-array
lpt1	lp-array	v	lp-array
lpt2	lp-array	v	lp-array
lptfun	lp-array	v	lprops → lprops
m	nat-basic1	v	nat
m0	lprops	v	nat
m1	lprops	v	nat
m2	lprops	v	nat
m3	lprops	v	nat
m4	lprops	v	nat
mklist	nat-list	f	nat × nat → nat-list
mklp	lprops	f	nat × nat × lpropflags × nat → lprops
mklparray	lp-array	f	nat → lp-array
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
n2	nat-set	v	nat
n3	nat-set	v	nat
n4	nat-set	v	nat
n5	nat-list	v	nat
nat	nat-basic1	s
nat-list	nat-list	s
nat-set	nat-set	s
ns	nat-set	v	nat-set
ns0	nat-set	v	nat-set
ns1	nat-set	v	nat-set
ns2	nat-set	v	nat-set
nx	nat-list	v	nat-list
nx0	nat-list	v	nat-list
nx1	nat-list	v	nat-list
nx2	nat-list	v	nat-list
ny	nat-list	v	nat-list
ny0	nat-list	v	nat-list
ny1	nat-list	v	nat-list
ny2	nat-list	v	nat-list
nz	nat-list	v	nat-list
nz0	nat-list	v	nat-list
nz1	nat-list	v	nat-list
nz2	nat-list	v	nat-list
pos	nat-list	f	nat × nat-list → nat
restn	nat-list	f	nat × nat-list → nat-list
rev	nat-list	f	nat-list → nat-list
rev	lp-array	f	lp-array × nat → lp-array
rev	lp-array	f	lp-array → lp-array
rmdup	nat-list	f	nat-list → nat-list
subarray	lp-array	f	lp-array × nat × nat → lp-array
sublist	nat-list	f	nat × nat × nat-list → nat-list
valid-indices	lp-array	p	lp-array × nat-list