3 ms·
Im not in this field so this might not be a good question, but why integration with LEAN and not ACL2, which is already written in Common Lisp
by medo-bear 3y ago
Im not in this field so this might not be a good question, but why integration with LEAN and not ACL2, which is already written in Common Lisp
- daly 3y agoI worked with Nqthm and ACL2. They seem best adapted to hardware verification. LEAN is pushing the edge of undergrad mathematics.