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/Checking/SetConstruction.hs | |
| parent | b5237180718b7290957b4f4f966a316e09306d54 (diff) | |
Pin relational extensional schema
Diffstat (limited to 'source/Checking/SetConstruction.hs')
| -rw-r--r-- | source/Checking/SetConstruction.hs | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/source/Checking/SetConstruction.hs b/source/Checking/SetConstruction.hs index 2a0c867..4c4b4bc 100644 --- a/source/Checking/SetConstruction.hs +++ b/source/Checking/SetConstruction.hs @@ -413,9 +413,10 @@ relationalSetConstructionClosedFunctionality relationalSetConstructionClosedFunctionality = closeRelationalFunctionality --- | Introduce a fresh named set. The caller must supply the exact checked --- functionality proposition it has admitted; no arbitrary proposition can --- unlock the derived extensional view. +-- | Introduce a fresh named set. Assuming the exact checked functionality +-- proposition, derive its two local views; no arbitrary proposition can +-- unlock the extensional view. The enclosing proof transaction owns the +-- corresponding authority. relationalSetConstructionLocalViews :: Ord global => SetConstructionFoundation |