Verifying Verifying Algorithm

Verifying Verifying Algorithm Impression about Lean4 I’ve been studying Lean for several weeks as a programming language and as a proof assistant, I would like to share my experience. My last Haskell project miso-css motivated me for the shift. It is a dependently typed HTML library that checks applicability of CSS classes to tags based on their ancestors and siblings and selectors. After finishing the library, I realized that no tool exists for library verification, due to its core logic si...