How was Idris' `rewrite` implemented?
I talked to be5invis and he said it's implemented using replace.

replace is something like this in Agda: $$ replace : \forall \{a \ b\} \rightarrow (a \equiv b) \rightarrow P \ a \rightarrow P \ b $$
or, using universal polymorphism: $$ replace : \forall \{n\} \{a \ b : Set \ n\} \rightarrow (a \equiv b) \rightarrow P \ a \rightarrow P \ b $$

This is obvious, in both Agda and Idris.

And we use it like this:

$$
\begin{align*}
&amp; proof : \ (a \equiv b) \rightarrow P \ a \rightarrow P \ b \\
&amp; proof \ theory \ pa = replace \ theory \ pa
\end{align*}
$$

While rewrite in is just a mixfix version of replace, so, the code above can be written like this:

$$
\begin{align*}
&amp; proof : \ (a \equiv b) \rightarrow P \ a \rightarrow P \ b \\
&amp; proof \ theory \ pa = rewrite \ theory \ in \ pa
\end{align*}
$$

In conclusion, rewrite is syntax sugar which desugars to replace, while replace is a library function that can be implemented by anyone.
So there's nothing special.  

Actually, Idris desugars it to a function like this:

rewrite__impl : (P : a -&gt; Type) -&gt; x = y -&gt; P y -&gt; P x
rewrite__impl P Refl prf = prf