Hacker News new | ask | show | jobs
by octoberfranklin 2040 days ago
Er, no. Even Coq proofs are written in an untyped language (Ltac). You've got your levels mixed up.