diff options
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 |