Skip to content
Snippets Groups Projects

Enforce sorting of concrete sets and maps during typing

Merged Raphaël Cauderlier requested to merge rafoo@sorted_maps into dev
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

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Guillaume Claret
  • Guillaume Claret
  • 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

    Compare with previous version

  • Raphaël Cauderlier resolved all threads

    resolved all threads

  • added 1 commit

    • ffe6f68d - Apply 1 suggestion(s) to 1 file(s)

    Compare with previous version

  • added 1 commit

    • 4c83fa87 - [michocoq] Enforce concrete maps and big maps to be sorted by construction

    Compare with previous version

  • Guillaume Claret approved this merge request

    approved this merge request

  • Please register or sign in to reply
    Loading