equal
deleted
inserted
replaced
35 variables are given |
35 variables are given |
36 |
36 |
37 - nominal_induct cannot avoid a term (for example function applied |
37 - nominal_induct cannot avoid a term (for example function applied |
38 to an argument). |
38 to an argument). |
39 |
39 |
|
40 - .induct and .exhaust could be the default methods for induction/cases |
|
41 on nominal datatypes |
|
42 |
40 Other: |
43 Other: |
41 |
44 |
42 - nested recursion, like types "trm list" in a constructor |
45 - nested recursion, like types "trm list" in a constructor |
43 |
46 |
44 - store information about defined nominal datatypes, so that |
47 - store information about defined nominal datatypes, so that |