equal
deleted
inserted
replaced
15 codatatype (sset: 'a) stream (map: smap rel: stream_all2) = |
15 codatatype (sset: 'a) stream (map: smap rel: stream_all2) = |
16 Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) |
16 Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) |
17 |
17 |
18 declaration {* |
18 declaration {* |
19 Nitpick_HOL.register_codatatype |
19 Nitpick_HOL.register_codatatype |
20 @{typ "'stream_element_type stream"} @{const_name stream_case} [dest_Const @{term Stream}] |
20 @{typ "'a stream"} @{const_name stream_case} [dest_Const @{term Stream}] |
21 (*FIXME: long type variable name required to reduce the probability of |
|
22 a name clash of Nitpick in context. E.g.: |
|
23 context |
|
24 fixes x :: 'stream_element_type |
|
25 begin |
|
26 |
|
27 lemma "sset s = {}" |
|
28 nitpick |
|
29 oops |
|
30 |
|
31 end |
|
32 *) |
|
33 *} |
21 *} |
34 |
22 |
35 code_datatype Stream |
23 code_datatype Stream |
36 |
24 |
37 lemma stream_case_cert: |
25 lemma stream_case_cert: |