[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
. !	remtau	f	('a → Option('e)) → Stream('a) → Stream('e)
. !	remtau	f	('a → Option('e)) → List('a) → List('e)
. '	list	f	'a → List('a)
. + .	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
. + .	remtau	f	Option('e) × Stream('e) → Stream('e)
. ++ .	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)
. .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
. .ext	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 'a → Option('e)
. .f	stream-basic	pf	Stream('a) → Nat → 'a with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. .foldLeft ( . )	list	f	List('a) × 'b × ('b × 'a → 'b) → 'b
. .get	option	pf	Option('a) → 'a with λ opt. opt ≠ None
. .getOrElse ( . )	option	f	Option('a) × 'a → 'a
. .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 ( . )	option	f	Option('a) × ('a → 'b) → Option('b)
. .map ( . )	list	f	List('a) × ('a → 'b) → List('b)
. .n	nat-inf	pf	Natinf → Nat with λ n∞. n∞ ≠ ∞
. .start	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 's → Bool
. .step	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 's × 'a × 's → Bool
. .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
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List('a) × List('a)
. < .	nat-inf	p	Natinf × Natinf
. > .	nat	p	Nat × Nat
. [ . := . ]	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⌝ < # σ
. [ . ]	list-getput	pf	List('a) × Nat → 'a with λ x, n. n < # x
. [ . ]	stream	pf	Stream('a) × Nat → 'a with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. ∈ .	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)
. o .	option	f	('b → Option('c)) × ('a → Option('b)) → 'a → Option('c)
[]	list-data	c	List('a)
[]	stream	c	Stream('a)
α	IOtrace	v	Stream('a)
β	IOtrace	v	Stream('e)
σ	IOtrace	v	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
IOAut	IO-Aut-data	f	('s → Bool) × ('s × 'a × 's → Bool) × ('a → Option('e)) → IOAutomaton('s, 'a, 'e)
IOAut?	IO-Automaton	p	IOAutomaton('s, 'a, 'e)
IOAutomaton	IO-Aut-data	s
List	list-data	s
Nat	nat-basic	s
Natinf	nat-inf	s
None	option	c	Option('a)
Option	option	s
Some	option	f	'a → Option('a)
Stream	stream-basic	s
a	IOtrace	v	'a
af	IOtrace	v	Nat → 'a
al	IOtrace	v	List('a)
alf	IOtrace	v	Nat → List('a)
disj	list-dup	p	List('a) × List('a)
dups	list-dup	p	List('a)
e	IOtrace	v	'e
ef	IOtrace	v	Nat → 'e
el	IOtrace	v	List('e)
exec	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
exec*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
execω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
ext	IOtrace	v	'a → Option('e)
fillfirst	list-last	f	Nat × 'a × List('a) → List('a)
finp	stream-basic	p	Stream('a)
frag	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
frag*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
fragω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
fragv	IOtrace	v	Stream('s) × Stream('a) → Bool
frome	list-del	f	List('a) × 'a → List('a)
hd	stream	pf	Stream('a) → 'a with λ σ. σ ≠ []
iNV	IOtrace	v	's → Bool
ii	IOtrace	v	Nat → Nat
ioa	IOtrace	v	IOAutomaton('s, 'a, 'e)
m	IOtrace	v	Nat
min	nat-inf	f	Natinf × Natinf → Natinf
mklist	list-last	f	'a × Nat → List('a)
move	IOtrace	f	IOAutomaton('s, 'a, 'e) → 's × List('e) × 's → Bool
movev	IOtrace	v	's × Stream('e) × 's → Bool
n	IOtrace	v	Nat
oe	IOtrace	v	Option('e)
oinj	option	p	('a → Option('b))
osurj	option	p	('a → Option('b))
rev	list-last	f	List('a) → List('a)
s	IOtrace	v	's
sf	IOtrace	v	Nat → 's
sl	IOtrace	v	List('s)
slf	IOtrace	v	Nat → List('s)
start	IOtrace	v	's → Bool
step	IOtrace	v	's × 'a × 's → Bool
tl	stream	pf	Stream('a) → Stream('a) with λ σ. σ ≠ []
trace	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('e) → Bool
trace*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('e) → Bool
traceω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 'e) → Bool
tracev	IOtrace	v	Stream('e) → Bool