[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
# .	list-data	f	List[A] → Nat
# .	stream	f	Stream[A] → Natinf
. '	list	f	A → List[A]
. ( . )	list-getput	pf	List[A] × Nat → A with λ x, n. n < # x
. ( . )	stream	pf	Stream[A] × Nat → A with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. ( . := . )	list-getput	pf	List[A] × Nat × A → List[A] with λ x, n, a. n < # x
. ( . := . )	stream	pf	Stream[A] × Nat × A → Stream[A] with λ σ, n, a. finp(σ) → ⌜n⌝ < # σ
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-data	f	A × List[A] → List[A]
. + .	list	f	List[A] × List[A] → List[A]
. + .	list	f	List[A] × A → List[A]
. + .	nat-inf	f	Natinf × Natinf → Natinf
. + .	stream	f	A × Stream[A] → Stream[A]
. + .	stream	f	Stream[A] × Stream[A] → Stream[A]
. + .	stream	f	List[A] × (Nat → A) → Nat → A
. ++ .	list-dup	f	List[A] × A → List[A]
. +1	nat-basic	f	Nat → Nat
. +2 .	list	f	A × A → List[A]
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	list-del	f	List[A] × A → List[A]
. -l .	list-del	f	List[A] × A → List[A]
. -p .	list-del	f	List[A] × Nat → List[A]
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List('A) × List('A)
. < .	nat-inf	p	Natinf × Natinf
. > .	nat	p	Nat × Nat
. ∈ .	list	p	'A × List('A)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊑ .	list-last	p	List('A) × List('A)
. ⊑ .	stream	p	Stream('A) × Stream('A)
. ⊒ .	list-last	p	List('A) × List('A)
. butlast	list-last	pf	List[A] → List[A] with λ x. x ≠ []
. distinct	list-dup	f	List[A] → List[A]
. drop ( . )	stream	f	(Nat → A) × Nat → Nat → A
. drop ( . )	list-del	pf	List[A] × Nat → List[A] with λ x, n. n ≤ # x
. drop ( . )	stream	pf	Stream[A] × Nat → Stream[A] with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. dropRight ( . )	list-last	pf	List[A] × Nat → List[A] with λ x, n. n ≤ # x
. f	stream-basic	pf	Stream[A] → Nat → A with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. foldLeft ( . )	list	f	List[A] × B × (B × A → B) → B
. head	list-data	pf	List[A] → A with λ x. x ≠ []
. indexOf ( . )	list-del	f	List[A] × A → Nat
. l	stream-basic	pf	Stream[A] → List[A] with λ σ. finp(σ)
. last	list-last	pf	List[A] → A with λ x. x ≠ []
. map ( . )	list	f	List[A] × (A → B) → List[B]
. n	nat-inf	pf	Natinf → Nat with λ n∞. n∞ ≠ ∞
. sublist ( . )	list-del	pf	List[A] × Nat × Nat → List[A] with λ x, n, m. n + m ≤ # x
. tail	list-data	pf	List[A] → List[A] with λ x. x ≠ []
. take ( . )	stream	f	(Nat → A) × Nat → List[A]
. take ( . )	list-del	pf	List[A] × Nat → List[A] with λ x, n. n ≤ # x
. take ( . )	stream	pf	Stream[A] × Nat → List[A] with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. take ( . )	stream	pf	Stream[A] × Natinf → Stream[A] with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
. takeRight ( . )	list-del	pf	List[A] × Nat → List[A] with λ x, n. n ≤ # x
[]	list-data	c	List[A]
[]	stream	c	Stream[A]
α	contfun-lim	v	Stream[A]
αf	contfun-lim	v	Nat → Stream[A]
αp	contfun-lim	v	Stream[A] → Bool
β	contfun-lim	v	Stream[B]
βf	contfun-lim	v	Stream[S] × Stream[A] → Stream[B]
σ	contfun-lim	v	Stream[S]
σf	contfun-lim	v	Nat → Stream[S]
∞	nat-inf	c	Natinf
⌜ . ⌝	stream-basic	f	List[A] → Stream[A]
⌜ . ⌝	stream-basic	f	(Nat → A) → Stream[A]
⌜ . ⌝	nat-inf	f	Nat → Natinf
List	list-data	s
Nat	nat-basic	s
Natinf	nat-inf	s
Stream	stream-basic	s
a	contfun-lim	v	A
af	contfun-lim	v	Nat → A
al	contfun-lim	v	List[A]
alf	contfun-lim	v	Nat → List[A]
alp	contfun-lim	v	List[A] → Bool
b	contfun-lim	v	B
bf	contfun-lim	v	Nat → B
bl	contfun-lim	v	List[B]
cont	contfun-lim	p	(Stream('A) → Stream('B))
cont	contfun-lim	p	(Stream('S) × Stream('A) → Stream('B))
disj	list-dup	p	List('A) × List('A)
dups	list-dup	p	List('A)
f	contfun-lim	v	Stream[A] → Stream[B]
fillfirst	list-last	f	Nat × A × List[A] → List[A]
finp	stream-basic	p	Stream('A)
frome	list-del	f	List[A] × A → List[A]
hd	stream	pf	Stream[A] → A with λ σ. σ ≠ []
lf	contfun-lim	v	List[A] → List[B]
lift	contfun-lim	f	(List[A] → Bool) → Stream[A] → Bool
lift	contfun-lim	f	(List[S] × List[A] → Bool) → Stream[S] × Stream[A] → Bool
lift	contfun-lim	pf	(List[A] → List[B]) → Stream[A] → Stream[B] with λ lf. λ α. mon(lf)
lift	contfun-lim	pf	(List[S] × List[A] → List[B]) → Stream[S] × Stream[A] → Stream[B] with λ trf. λ σ, α. mon(trf)
lifted	contfun-lim	f	(List[A] → Bool) → (List[A] → List[B]) × (Stream[A] → Stream[B]) → Bool
lifted	contfun-lim	f	(List[S] × List[A] → Bool) → (List[S] × List[A] → List[B]) × (Stream[S] × Stream[A] → Stream[B]) → Bool
lim	streamseq-mon-lim	pf	Stream[Stream[A]] → Stream[A] with λ σσ. mon(σσ) ∧ σσ ≠ []
m	contfun-lim	v	Nat
min	nat-inf	f	Natinf × Natinf → Natinf
mklist	list-last	f	A × Nat → List[A]
mon	streamseq-mon-lim	p	Stream(Stream('A))
mon	contfun-lim	p	(Stream('A) → Stream('B))
mon	contfun-lim	p	(Stream('S) × Stream('A) → Stream('B))
mon	contfun-lim	p	(List('A) → List('B))
mon	contfun-lim	p	(List('S) × List('A) → List('B))
n	contfun-lim	v	Nat
pbd	contfun-lim	p	(Stream('A) → Stream('B))
pbd	contfun-lim	p	(Stream('S) × Stream('A) → Stream('B))
pcont	contfun-lim	f	(Stream[A] → Bool) → (Stream[A] → Stream[B]) → Bool
pcont	contfun-lim	f	(Stream[S] × Stream[A] → Bool) → (Stream[S] × Stream[A] → Stream[B]) → Bool
pfxclosed	contfun-lim	p	(Stream('A) → Bool)
pfxclosed	contfun-lim	p	(List('A) → Bool)
pfxclosed	contfun-lim	p	(Stream('S) × Stream('A) → Bool)
pfxclosed	contfun-lim	p	(List('S) × List('A) → Bool)
pmon	contfun-lim	f	(Stream[A] → Bool) → (Stream[A] → Stream[B]) → Bool
pmon	contfun-lim	f	(List[A] → Bool) → (List[A] → List[B]) → Bool
pmon	contfun-lim	f	(Stream[S] × Stream[A] → Bool) → (Stream[S] × Stream[A] → Stream[B]) → Bool
pmon	contfun-lim	f	(List[S] × List[A] → Bool) → (List[S] × List[A] → List[B]) → Bool
ppbd	contfun-lim	f	(Stream[A] → Bool) → (Stream[A] → Stream[B]) → Bool
ppbd	contfun-lim	f	(Stream[S] × Stream[A] → Bool) → (Stream[S] × Stream[A] → Stream[B]) → Bool
rev	list-last	f	List[A] → List[A]
sf	contfun-lim	v	Nat → S
sl	contfun-lim	v	List[S]
slf	contfun-lim	v	Nat → List[S]
tl	stream	pf	Stream[A] → Stream[A] with λ σ. σ ≠ []
trf	contfun-lim	v	List[S] × List[A] → List[B]
trlp	contfun-lim	v	List[S] × List[A] → Bool
trp	contfun-lim	v	Stream[S] × Stream[A] → Bool