From 948ff951bc161c10e021477e964e1a4a766ed598 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Fri, 27 Feb 2026 06:46:22 +0000
Subject: [PATCH] chore: add li op

---
 RISCV/Instructions.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/RISCV/Instructions.lean b/RISCV/Instructions.lean
index 0bfd22f..8baa71a 100644
--- a/RISCV/Instructions.lean
+++ b/RISCV/Instructions.lean
@@ -7,6 +7,13 @@ namespace RV64
 
 /-! # RV64I Base Integer Instruction Set -/
 
+/--
+  Load a 64-wide immediate into the destination register rd
+-/
+def li (imm : BitVec 64) : BitVec 64 :=
+  imm
+
+
 /--
   Build 32-bit constants and uses the U-type format. LUI places the U-immediate value in the top 20
   bits of the destination register rd, filling in the lowest 12 bits with zeros.