File tree Expand file tree Collapse file tree 1 file changed +1
-1
lines changed Expand file tree Collapse file tree 1 file changed +1
-1
lines changed Original file line number Diff line number Diff line change 5454< a id ="1432 " class ="Comment "> ------------------------------------------------------------------------</ a >
5555< a id ="1505 " class ="Comment "> -- Setoid bundles</ a >
5656
57- < a id ="1524 " class ="Keyword "> module</ a > < a id ="1531 " href ="Function.Construct.Constant.html#1531 " class ="Module "> _</ a > < a id ="1533 " class ="Symbol "> (</ a > < a id ="1534 " href ="Function.Construct.Constant.html#1534 " class ="Bound "> S</ a > < a id ="1536 " class ="Symbol "> :</ a > < a id ="1538 " href ="Relation.Binary.Bundles.html#1235 " class ="Record "> Setoid</ a > < a id ="1545 " href ="Function.Construct.Constant.html#715 " class ="Generalizable "> a</ a > < a id ="1547 " href ="Function.Construct.Constant.html#722 " class ="Generalizable "> ℓ₂ </ a > < a id ="1549 " class ="Symbol "> )</ a > < a id ="1551 " class ="Symbol "> (</ a > < a id ="1552 " href ="Function.Construct.Constant.html#1552 " class ="Bound "> T</ a > < a id ="1554 " class ="Symbol "> :</ a > < a id ="1556 " href ="Relation.Binary.Bundles.html#1235 " class ="Record "> Setoid</ a > < a id ="1563 " href ="Function.Construct.Constant.html#717 " class ="Generalizable "> b</ a > < a id ="1565 " href ="Function.Construct.Constant.html#722 " class ="Generalizable "> ℓ₂</ a > < a id ="1567 " class ="Symbol "> )</ a > < a id ="1569 " class ="Keyword "> where</ a >
57+ < a id ="1524 " class ="Keyword "> module</ a > < a id ="1531 " href ="Function.Construct.Constant.html#1531 " class ="Module "> _</ a > < a id ="1533 " class ="Symbol "> (</ a > < a id ="1534 " href ="Function.Construct.Constant.html#1534 " class ="Bound "> S</ a > < a id ="1536 " class ="Symbol "> :</ a > < a id ="1538 " href ="Relation.Binary.Bundles.html#1235 " class ="Record "> Setoid</ a > < a id ="1545 " href ="Function.Construct.Constant.html#715 " class ="Generalizable "> a</ a > < a id ="1547 " href ="Function.Construct.Constant.html#719 " class ="Generalizable "> ℓ₁ </ a > < a id ="1549 " class ="Symbol "> )</ a > < a id ="1551 " class ="Symbol "> (</ a > < a id ="1552 " href ="Function.Construct.Constant.html#1552 " class ="Bound "> T</ a > < a id ="1554 " class ="Symbol "> :</ a > < a id ="1556 " href ="Relation.Binary.Bundles.html#1235 " class ="Record "> Setoid</ a > < a id ="1563 " href ="Function.Construct.Constant.html#717 " class ="Generalizable "> b</ a > < a id ="1565 " href ="Function.Construct.Constant.html#722 " class ="Generalizable "> ℓ₂</ a > < a id ="1567 " class ="Symbol "> )</ a > < a id ="1569 " class ="Keyword "> where</ a >
5858
5959 < a id ="1578 " class ="Keyword "> open</ a > < a id ="1583 " href ="Relation.Binary.Bundles.html#1235 " class ="Module "> Setoid</ a >
6060
You can’t perform that action at this time.
0 commit comments