So, I just tried running LEAN (Lean theorem prover. Link ), and, I am quite confused by how much of my computer’s processor it used.
made the file with the content:
constant m : nat
#check m
lean --run ..\..\progs\test1.lean
Which brought my PC’s cpu usage from ~20% to varying between 80% and 100% , to eventually produce the output:
m : Γäò
<unknown>:1:1: error: unknown declaration 'main'
(Which, saying “ Γäò “ was presumably just because windows command line can’t display the symbol for the natural numbers, so that isn’t an issue by itself.)
But, it look like a minute to come up with that output, and it brought my pc’s CPU usage to 100% . I don’t understand why.
Shouldn’t this be an extremely simple thing to run?
Can anyone tell me what I am doing wrong here?