• edinbruh
    link
    fedilink
    English
    arrow-up
    3
    ·
    6 days ago

    Stop doing lean! Computers weren’t meant to do classic logics!

    Embrace rocq (formerly coq), for pure constructive logic! Plus the syntax is nicer