Enforce sorting of concrete sets and maps during typing
All threads resolved!
All threads resolved!
Solves #28 (closed).
The representation of concrete data and data of type set and map are now uniform, sorting is checked by the typer.
This required a massive refactoring of the map module to change the definition to something accepted by the strict positivity criterion in the definition of syntax.concrete_data
.
Merge request reports
Activity
Filter activity
changed milestone to %beta-release
added formalisation label
added 16 commits
-
291c5491...5796046f - 11 commits from branch
dev
- e23e1fe8 - [michocoq|extraction] fix a typo
- 5c880ee9 - [michocoq] Reverse dependency between syntax.v and comparable.v
- 96b587fc - [michocoq] Use simple_comparable_data to simplify concrete_data
- 89260945 - [michocoq] Enforce ordering of concrete sets
- f69f4191 - [michocoq] Enforce concrete maps and big maps to be sorted by construction
Toggle commit list-
291c5491...5796046f - 11 commits from branch
assigned to @julien.t
added 6 commits
-
a4d37fa7 - 1 commit from branch
dev
- 7a465529 - [michocoq|extraction] fix a typo
- 19508c96 - [michocoq] Reverse dependency between syntax.v and comparable.v
- e6763ec7 - [michocoq] Use simple_comparable_data to simplify concrete_data
- 2e6f1d83 - [michocoq] Enforce ordering of concrete sets
- 9ffcc52e - [michocoq] Enforce concrete maps and big maps to be sorted by construction
Toggle commit list-
a4d37fa7 - 1 commit from branch
- Resolved by Raphaël Cauderlier
- Resolved by Raphaël Cauderlier
- Resolved by Raphaël Cauderlier
mentioned in issue #28 (closed)
added 6 commits
-
5a01c812 - 1 commit from branch
dev
- d89caaff - [michocoq|extraction] fix a typo
- 760fbfec - [michocoq] Reverse dependency between syntax.v and comparable.v
- 1df31922 - [michocoq] Use simple_comparable_data to simplify concrete_data
- fe8c6f05 - [michocoq] Enforce ordering of concrete sets
- 344ee379 - [michocoq] Enforce concrete maps and big maps to be sorted by construction
Toggle commit list-
5a01c812 - 1 commit from branch
added 1 commit
- 4c83fa87 - [michocoq] Enforce concrete maps and big maps to be sorted by construction
Please register or sign in to reply