| Symbol | Specification | Kind | Type |
|---|
| . .ext | IO-Aut-data | f | IOAutomaton('s, 'a, 'e) → 'a → Option('e) |
| . .get | option | pf | Option('a) → 'a with λ opt. opt ≠ None |
| . .getOrElse ( . ) | option | f | Option('a) × 'a → 'a |
| . .map ( . ) | option | f | Option('a) × ('a → 'b) → Option('b) |
| . .start | IO-Aut-data | f | IOAutomaton('s, 'a, 'e) → 's → Bool |
| . .step | IO-Aut-data | f | IOAutomaton('s, 'a, 'e) → 's × 'a × 's → Bool |
| . o . | option | f | ('b → Option('c)) × ('a → Option('b)) → 'a → Option('c) |
| . o . | funops | f | ('a → 'b) × ('b → 'c) → 'a → 'c |
| Π | product | f | ('ls → Bool) × ('rs → Bool) → ('ls, 'rs) → Bool |
| Π | product | f | ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) × ('la → 'pa) × ('ra → 'pa) ×
('la → Option('e)) × ('ra → Option('e))
→ ('ls, 'rs) × 'pa × ('ls, 'rs) → Bool |
| Π | product | f | ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) → 'pa → Option('e) |
| Π | product | pf | IOAutomaton('ls, 'la, 'e) × IOAutomaton('rs, 'ra, 'e) × ('la → 'pa) × ('ra → 'pa)
→ IOAutomaton(('ls, 'rs), 'pa, 'e) with λ lioaut, rioaut, lren, rren. Πok(lioaut.ext, rioaut.ext, lren, rren) |
| Πh | product | f | ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) × ('e → Option('f))
→ 'pa → Option('f) |
| Πh | product | pf | IOAutomaton('ls, 'la, 'e) × IOAutomaton('rs, 'ra, 'e) × ('la → 'pa) × ('ra → 'pa) ×
('e → Option('f))
→ IOAutomaton(('ls, 'rs), 'pa, 'f) with λ lioaut, rioaut, lren, rren, hideext. Πhok(lioaut.ext, rioaut.ext, lren, rren, hideext) |
| Πhok | product | p | ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) × ('e → Option('f)) |
| Πok | product | p | ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) |
| 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 | |
| None | option | c | Option('a) |
| Option | option | s | |
| Some | option | f | 'a → Option('a) |
| a | product | v | 'a |
| cod | funops | f | ('a → 'b) → 'b → Bool |
| e | product | v | 'e |
| hideext | product | v | 'e → Option('f) |
| hidingok | product | p | ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) × ('e → Option('f)) |
| inj | funops | p | ('a → 'b) |
| la | product | v | 'la |
| lext | product | v | 'la → Option('e) |
| lioaut | product | v | IOAutomaton('ls, 'la, 'e) |
| lren | product | v | 'la → 'pa |
| ls | product | v | 'ls |
| lstart | product | v | 'ls → Bool |
| lstep | product | v | 'ls × 'la × 'ls → Bool |
| oinj | option | p | ('a → Option('b)) |
| osurj | option | p | ('a → Option('b)) |
| pa | product | v | 'pa |
| pext | product | v | 'pa → Option('e) |
| pioaut | product | v | IOAutomaton(('ls, 'rs), 'pa, 'e) |
| ps | product | v | ('ls, 'rs) |
| pstart | product | v | ('ls, 'rs) → Bool |
| pstep | product | v | ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) → ('ls, 'rs) × 'pa × ('ls, 'rs) → Bool |
| ra | product | v | 'ra |
| ren | product | v | 'a → 'b |
| rext | product | v | 'ra → Option('e) |
| rioaut | product | v | IOAutomaton('rs, 'ra, 'e) |
| rren | product | v | 'ra → 'pa |
| rs | product | v | 'rs |
| rstart | product | v | 'rs → Bool |
| rstep | product | v | 'rs × 'ra × 'rs → Bool |
| sharingok | product | p | ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) |
| surj | funops | p | ('a → 'b) |
| surj | product | p | ('la → 'pa) × ('ra → 'pa) |