Rename RVec and Rvec to avoid windows case-insensitive shenanigans

parent 0f3203b3
\begin{code}
module Data.RVec where
module Data.RDataVec where
open import Level using (_⊔_; Lift; lift) renaming (suc to lsuc)
......
\begin{code}
module Data.Rvec where
module Data.RFunctionVec where
\end{code}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment