File tree Expand file tree Collapse file tree 1 file changed +15
-0
lines changed Expand file tree Collapse file tree 1 file changed +15
-0
lines changed Original file line number Diff line number Diff line change @@ -29,6 +29,21 @@ Non-backwards compatible changes
29
29
library. This allowed them to be used in the rest of library where
30
30
explicit ` Lift ` was used.
31
31
32
+ * The representation of reflected syntax in ` Reflection.Term ` and
33
+ ` Reflection.Pattern ` has been updated to match the new
34
+ representation used in Agda 2.6.2. Specifically, the following changes were made:
35
+
36
+ * The type of the ` var ` constructor of the ` Pattern ` datatype has
37
+ been changed from ` (x : String) → Pattern ` to `(x : Int) →
38
+ Pattern`.
39
+ * The type of the ` dot ` constructor of the ` Pattern ` datatype has
40
+ been changed from ` Pattern ` to ` (t : Term) → Pattern `
41
+ * The types of the ` clause ` and ` absurd-clause ` constructors of the
42
+ ` Clause ` datatype now take an extra argument ` (tel : Telescope) ` ,
43
+ where ` Telescope = List (String × Arg Type) ` .
44
+
45
+ See the release notes of Agda 2.6.2 for more information.
46
+
32
47
Deprecated modules
33
48
------------------
34
49
You can’t perform that action at this time.
0 commit comments