How was Idris' `rewrite` implemented?

Question

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?