<html><body><div style="color:#000; background-color:#fff; font-family:times new roman, new york, times, serif;font-size:12pt"><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; ">Hello Ramana</div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "><br></div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; ">Could you motivate your definition a bit more?</div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; ">I don't have much idea what it should mean.</div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; ">It seems very similar to a this definition,</div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; ">which I am not surprised to see rejected</div><div style="font-family: 'times new roman', 'new york', times, serif; font-size:
12pt; "><br></div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "><span style="font-size: 12pt; ">data foo : (y : Bool) -> Bool where</span><br></div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; ">-- no constructors</div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "><br></div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; ">If the idea is to have an inductive family where some indices</div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; ">live at different levels, you might compare to this definition:</div><div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "><br></div><div><div>data foo : (y : Bool) → Set (if y then zero else suc zero) where</div><div> bar : foo true</div><div><br></div><div>which produces
a more straightforward error message</div><div><br></div></div><div><div>home/brandon/test/test.agda:5,6-9</div><div>The sort of foo cannot depend on its indices in the type (y : Bool)</div><div>→ Set (if y then zero else suc zero)</div><div>when checking the definition of foo</div><div><br></div><div>Brandon</div></div> </div></body></html>