How was Idris' `rewrite` implemented?

I know in Agda, rewrite is a syntax sugar that desugars to a with abstraction.

For example, if we have (I'm using the Data.Vec from the standard library):

$$
\DeclareMathOperator{Set}{Set}
\DeclareMathOperator{xs}{xs}
\DeclareMathOperator{where}{where}
\DeclareMathOperator{proof}{proof}
\DeclareMathOperator{data}{data}
\DeclareMathOperator{rev}{rev}
\DeclareMathOperator{ff}{ff}
\DeclareMathOperator{lemma}{lemma}
\DeclareMathOperator{intro}{intro}
\DeclareMathOperator{id}{id}
\DeclareMathOperator{refl}{refl}
\DeclareMathOperator{params}{params}
\DeclareMathOperator{Vec}{Vec}
\DeclareMathOperator{rewrite}{rewrite}
\DeclareMathOperator{with}{with}
\DeclareMathOperator{revrevid}{revrevid}
\begin{align*}
& \revrevid : \forall \{n \ m\} \{A : \Set n\}
(a : A) (v : \Vec A \ m) \rightarrow
\rev (v \ {:}{:} ^r a) \equiv a \ {:}{:}\rev v \\
& \revrevid \ \_ \ [] = \refl \\
& \revrevid \ a \ (\_ \ {:}{:} \ \xs) \ \rewrite \revrevid \ a \ \xs = \refl
\end{align*}
$$

This will be desugared to:

$$
\begin{align*}
& \revrevid : \forall \{n \ m\} \{A : \Set n\}
(a : A) (v : \Vec A \ m) \rightarrow
\rev (v \ {:}{:} ^r a) \equiv a \ {:}{:}\rev v \\
& \revrevid \ \_ \ [] = \refl \\
& \revrevid \ a \ (\_ \ {:}{:} \ \xs) \with \ \rev (\xs \ {:}{:}^r \ a) \ | \ \revrevid \ a \ \xs \\
& ... \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | \ {.}(a \ {:}{:} \rev \xs) \ | \refl = \refl
\end{align*}
$$

But in Idris, there's nothing like a with abstraction, or a dot pattern (which are available in Agda).

So how does Idris' rewrite implemented? Is that just a syntax sugar or a language feature which cannot be implemented in pure Idris code?

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*}
& proof : \ (a \equiv b) \rightarrow P \ a \rightarrow P \ b \\
& 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*}
& proof : \ (a \equiv b) \rightarrow P \ a \rightarrow P \ b \\
& 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 -> Type) -> x = y -> P y -> P x
rewrite__impl P Refl prf = prf

StackExchange Computer Science Q#84486, answer score: 4