Post History

# [Lean 4], 232 bytes

```lean
def r(i):=Id.run do
let M:=[999,899,499,399,99,89,49,39,9,8,4,3,0]
let N:=["M","CM","D","CD","C","XC","L","XL","X","IX","V","IV","I"]
let mut s:=""
let mut n:=i
for x in List.range 13do while n>M[x]do s:=s++N[x];n:=n-M[x]-1
return s
```
Note that you will need to run this with `#eval!` instead of `#eval` since I never proved that the list indexes are valid (although this is entirely optional).

The reason I can't simply combine the two lists is because that is simply something that Lean doesn't allow. While I can combine different types using tuples, the problem there is that I can't index tuples.

---

[Try it online](https://live.lean-lang.org/#codez=CYUwZgBATgFAlgSgFwF4CSwB0UCuA7CYAewCgAbEAFwgFlUBtATmYBoAOVgFlYGZXWOLbiz4tG7ISJYAGALrkqEAHIMARDVUtVAYQ1aAIpp2Gt2owA0zWgDIXbW80bSOtANSfutaVfIrUAtjjUAM6oqqoKAUEQeKhwJGBEUBAAHhBwBNZwwZTYAIZ4AOYgEACMPMQQAO4AFnAUMQB8NPQpspWhKMEA1N1KrbIA3LEoeAC0LW1jpSRQVDhQBMEkJADEIABueWQAhNAQAGxHQA)

[Lean 4]:https://github.com/leanprover/lean4