<div dir="ltr">(and to be sure, [abstract] keyword is not the issue here: 
this manifests no matter how you achieve abstraction: module parameter, lambda, whatever)<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 17 May 2018 at 00:01, Arseniy Alekseyev <span dir="ltr"><<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I'll point out that source-level stability under substitution is not even compatible with implicit parameters if unsolved metavariables is also something you care about.<div>For example the below program works with "abstract" and has unsolved metavariables without "abstract".</div><div><div><br></div><div><div><div>data Bool : Set where</div><div>  true false : Bool</div><div><br></div><div>abstract</div><div>  or : Bool → Bool → Bool</div><div>  or true _ = true</div><div>  or false x = x</div><div><br></div><div>data Is-bool : Bool → Set where</div><div>  is-bool : ∀ x → Is-bool x</div><div><br></div><div>contrived : ∀ {x} → Is-bool (or x true) → Bool</div><div>contrived {x} _ = x</div><div><br></div><div>z = contrived (is-bool (or false true))</div></div></div></div><div><br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 16 May 2018 at 22:58, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><br>
<br>
On 16/05/18 22:55, <a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmai<wbr>l.com</a> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This is really scary, for good reason. It seems that we are in a better position now than a few years ago.<br>
<br>
I do remember as an undergraduate, thinking that all I need is to start from the fundamentals of Mathematics and then prove all of the rest.<br>
Then , I found that the fundamentals were full of paradoxes.<br>
<a href="https://en.wikipedia.org/wiki/Foundations_of_mathematics#Foundational_crisis" rel="noreferrer" target="_blank">https://en.wikipedia.org/wiki/<wbr>Foundations_of_mathematics#Fou<wbr>ndational_crisis</a><br>
</blockquote>
<br></span>
Agda is an incarnation of both established type theories and frontier research on possible new type theories, and it is good that things are like this, because researchers can use it for experimentation.<br>
<br>
But some other researchers would like to use Agda to work with established type theories.<br>
<br>
It is good that Agda has some seat-belts such as --exact-split, --safe, and --without-K, for that purpose.<br>
<br>
Further seat-belts would be welcome.<br>
<br>
The point I was making was not about scariness but about awareness. If you use a feature beyond your type-theory expertise, consider whether this feature is well established, but unknown to you, or something experimental and perhaps not well-defined.<span class="m_-3923809028247396922HOEnZb"><font color="#888888"><br>
<br>
Martin</font></span><div class="m_-3923809028247396922HOEnZb"><div class="m_-3923809028247396922h5"><br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>