equal
deleted
inserted
replaced
5 |
5 |
6 theory DSequence |
6 theory DSequence |
7 imports Lazy_Sequence Code_Numeral |
7 imports Lazy_Sequence Code_Numeral |
8 begin |
8 begin |
9 |
9 |
10 types 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option" |
10 type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option" |
11 |
11 |
12 definition empty :: "'a dseq" |
12 definition empty :: "'a dseq" |
13 where |
13 where |
14 "empty = (%i pol. Some Lazy_Sequence.empty)" |
14 "empty = (%i pol. Some Lazy_Sequence.empty)" |
15 |
15 |