diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-05 17:55:31 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-05 17:55:31 +0200 |
| commit | 2f6b8a5033bed7736c54494d6f0cca98771cc9e0 (patch) | |
| tree | 4806d9a8c5b8d390c05f57d26085d891545c8293 /source/Test | |
| parent | b5237180718b7290957b4f4f966a316e09306d54 (diff) | |
Pin relational extensional schema
Diffstat (limited to 'source/Test')
| -rw-r--r-- | source/Test/Unit/Declaration.hs | 44 |
1 files changed, 42 insertions, 2 deletions
diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs index c64ef54..4c8c3f0 100644 --- a/source/Test/Unit/Declaration.hs +++ b/source/Test/Unit/Declaration.hs @@ -2434,6 +2434,30 @@ lowersExactReplacementTelescopes = do (Core.scopedCoreTerm (SetConstruction.relationalSetConstructionFunctionality construction)) + let relationalObject = + Identity.assertedObjectId + (opaqueFixtureObject fixture) + closedFunctionality = + SetConstruction.relationalSetConstructionClosedFunctionality + construction + relationalFact <- + maybe + (assertFailure + "exact functionality did not unlock relational extensionality" + >> fail "unreachable") + pure + (SetConstruction.relationalSetConstructionObjectFact + (SetConstruction.checkedFoundationSetConstruction + (fixtureFoundation fixture)) + relationalObject + construction + closedFunctionality) + assertEqual + "relational replacement flattened extensional proposition" + (expectedRelationalExtensional relationalObject) + (Core.frozenCoreTerm + (SetConstruction.relationalSetConstructionFactProposition + relationalFact)) assertEqual "unrelated functionality cannot unlock the relational view" Nothing @@ -2452,8 +2476,7 @@ lowersExactReplacementTelescopes = do (SetConstruction.relationalSetConstructionObjectFact (SetConstruction.checkedFoundationSetConstruction (fixtureFoundation fixture)) - (Identity.assertedObjectId - (opaqueFixtureObject fixture)) + relationalObject construction wrongClosed)) _ -> @@ -2512,6 +2535,23 @@ lowersExactReplacementTelescopes = do (Core.CBound 2) (Core.CBound 0))) (Core.CEq Core.TySet (Core.CBound 1) (Core.CBound 0)))))) + expectedRelationalExtensional object = + Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CEq Core.TyProp + (relApp2 Core.Member + (Core.CBound 0) + (Core.CApp + (Core.CGlobal object) + (Core.CBound 1))) + (existsP + (andP + (relApp2 Core.Member + (Core.CBound 0) + (Core.CBound 2)) + (Core.CEq Core.TySet + (Core.CBound 0) + (Core.CBound 1)))))) lowersExactFiniteSets :: Assertion lowersExactFiniteSets = do |