equal
deleted
inserted
replaced
14 Atom 'a | |
14 Atom 'a | |
15 Plus "('a rexp)" "('a rexp)" | |
15 Plus "('a rexp)" "('a rexp)" | |
16 Times "('a rexp)" "('a rexp)" | |
16 Times "('a rexp)" "('a rexp)" | |
17 Star "('a rexp)" |
17 Star "('a rexp)" |
18 |
18 |
19 primrec lang :: "'a rexp => 'a list set" where |
19 primrec lang :: "'a rexp => 'a lang" where |
20 "lang Zero = {}" | |
20 "lang Zero = {}" | |
21 "lang One = {[]}" | |
21 "lang One = {[]}" | |
22 "lang (Atom a) = {[a]}" | |
22 "lang (Atom a) = {[a]}" | |
23 "lang (Plus r s) = (lang r) Un (lang s)" | |
23 "lang (Plus r s) = (lang r) Un (lang s)" | |
24 "lang (Times r s) = conc (lang r) (lang s)" | |
24 "lang (Times r s) = conc (lang r) (lang s)" | |