<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p>Dear list,</p>
<p>I'm trying to write some simple code using sizes. Here is
something that I don't understand:</p>
<p><br>
</p>
<p>open import Size public<br>
<br>
record Test {i : Size} : Set where<br>
field<br>
test : {j : Size< i} → ?<br>
<br>
</p>
<br>
Take this code and try to load it. It will show the following error:<br>
<br>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<atom-panel class="agda-view bottom tool-panel panel-bottom"
style="box-sizing: border-box; display: block; position: relative;
font-weight: normal; color: rgb(68, 68, 68); text-shadow:
rgba(255, 255, 255, 0.498039) 0px 1px 0px; z-index: 4; height:
191px; border-top: 1px solid rgb(159, 159, 159); font-family:
BlinkMacSystemFont, "Lucida Grande", "Segoe
UI", Ubuntu, Cantarell, sans-serif; font-size: 11px;
font-style: normal; font-variant-ligatures: normal;
font-variant-caps: normal; letter-spacing: normal; line-height:
15.7143px; orphans: 2; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: 2;
word-spacing: 0px; -webkit-text-stroke-width: 0px;
background-color: rgb(244, 244, 244);">
<article style="box-sizing: border-box;">
<section data-reactroot="" class="" style="box-sizing:
border-box; position: relative; margin-top: 0px;
margin-bottom: 0px;">
<section class="agda-body-container" style="box-sizing: border-box; position: relative; margin: 0px; height: 140px; overflow-y: scroll; font-family: inconsolata, Menlo, Consolas, "DejaVu Sans Mono", "Liberation Mono", Monaco, "Lucida Console", monospace; padding: 0px 10px; font-size: 13.75px; white-space: pre-wrap;"><section class="native-key-bindings agda-body" tabindex="-1" style="box-sizing: border-box; position: relative; margin-top: 0px; outline: none; margin-bottom: 0px; max-height: 310px;"><p style="box-sizing: border-box; margin: 10px 0px; line-height: 30px; min-height: 30px; padding: 0px 10px;">Sort _2 [ at /....agda:5,28-35 ]
———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
dLub Set (λ j → Set _2) =< Set</p></section></section>
</section>
</article>
</atom-panel><atom-panel class="agda-view bottom tool-panel
panel-bottom" style="box-sizing: border-box; display: block;
position: relative; font-weight: normal; color: rgb(68, 68, 68);
text-shadow: rgba(255, 255, 255, 0.498039) 0px 1px 0px; z-index:
4; height: 1px; border-top: 1px solid rgb(159, 159, 159);
font-family: BlinkMacSystemFont, "Lucida Grande",
"Segoe UI", Ubuntu, Cantarell, sans-serif; font-size:
11px; font-style: normal; font-variant-ligatures: normal;
font-variant-caps: normal; letter-spacing: normal; line-height:
15.7143px; orphans: 2; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: 2;
word-spacing: 0px; -webkit-text-stroke-width: 0px;
background-color: rgb(244, 244, 244);">
<article style="box-sizing: border-box;"></article>
</atom-panel><atom-panel class="agda-view bottom tool-panel
panel-bottom" style="box-sizing: border-box; display: block;
position: relative; font-weight: normal; color: rgb(68, 68, 68);
text-shadow: rgba(255, 255, 255, 0.498039) 0px 1px 0px; z-index:
4; height: 1px; border-top: 1px solid rgb(159, 159, 159);
font-family: BlinkMacSystemFont, "Lucida Grande",
"Segoe UI", Ubuntu, Cantarell, sans-serif; font-size:
11px; font-style: normal; font-variant-ligatures: normal;
font-variant-caps: normal; letter-spacing: normal; line-height:
15.7143px; orphans: 2; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: 2;
word-spacing: 0px; -webkit-text-stroke-width: 0px;
background-color: rgb(244, 244, 244);">
<article style="box-sizing: border-box;"></article>
</atom-panel><atom-panel class="agda-view bottom tool-panel
panel-bottom" style="box-sizing: border-box; display: block;
position: relative; font-weight: normal; color: rgb(68, 68, 68);
text-shadow: rgba(255, 255, 255, 0.498039) 0px 1px 0px; z-index:
4; height: 1px; border-top: 1px solid rgb(159, 159, 159);
font-family: BlinkMacSystemFont, "Lucida Grande",
"Segoe UI", Ubuntu, Cantarell, sans-serif; font-size:
11px; font-style: normal; font-variant-ligatures: normal;
font-variant-caps: normal; letter-spacing: normal; line-height:
15.7143px; orphans: 2; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: 2;
word-spacing: 0px; -webkit-text-stroke-width: 0px;
background-color: rgb(244, 244, 244);">
<article style="box-sizing: border-box;"></article>
</atom-panel><br>
<br class="Apple-interchange-newline">
What's going on?<br>
<br>
Manuel<br>
<pre class="moz-signature" cols="72">--
I'm using Enigmail on Thunderbird to sign and encrypt my emails with GPG! Why not try it yourself? <a class="moz-txt-link-freetext" href="https://enigmail.net/">https://enigmail.net/</a></pre>
</body>
</html>