IntersectMBO / formal-ledger-specifications

Formal specifications of the cardano ledger

Apache License 2.0

38 stars 13 forks source link

Factor out the set theory into a separate library #592

Closed WhatisRT closed 1 month ago

WhatisRT commented 1 month ago

Description

This introduces a dependency of the new agda-sets. I also did some refactoring as part of this, which is where most changes come from.

I've requested reviews from everyone who I think might be interested, but feel free to ignore it or just have a quick look.

Checklist

[x] Commit sequence broadly makes sense and commits have useful messages
[x] Any semantic changes to the specifications are documented in CHANGELOG.md
[x] Code is formatted according to CONTRIBUTING.md
[x] Self-reviewed the diff

javierdiaz72 commented 1 month ago

I'm just curious regarding https://github.com/input-output-hk/agda-sets/blob/6dd8cebbd46090b5909c13a1e8d609a44f02a5d3/src/Axiom/Set/Predicates.agda#L1: Why is --type-in-type needed here? As I understand it (with my still limited experience in Agda), this flag renders the logic inconsistent.

Otherwise, the changes look good to me!

WhatisRT commented 1 month ago

Yes, --type-in-type is indeed inconsistent. It's necessary there only because of stupid reasons: In Theory, the field Set has type Type ℓ → Type ℓ, but λ A → A → Type has type Type ℓ → Type (ℓ ⊔ 1).

However, I've made this issue: https://github.com/input-output-hk/agda-sets/issues/2 Resolving that will allow dropping --type-in-type. So I'd say that in this case the inconsistency is something not to worry about.

WhatisRT commented 1 month ago

Yeah, sorry for the extra friction, but it's required for being able to use it it other projects. You can of course always add stuff in a module like Axiom.Set.Ext and then upstream it when it's done.