Congratulations on the big milestone! This really appeals to the same part of my brain that likes (to varying degrees) Haskell, Rust and TypeScript. Can Idris

Congratulations on the big milestone! This really appeals to the same part of my brain that likes (to varying degrees) Haskell, Rust and TypeScript. Can Idris be used as a Coq-style "proof assistant"? From reading http://docs.idris-lang.org/en/latest/reference/elaborator-reflection.html http://docs.idris-lang.org/en/latest/reference/elaborator-re... , it looks like there was an older proof system that has recently been replaced by something new, and I can't tell if Idris can still be used as Coq replacement. Are there good tutorials on this? EDIT: It seems like yes, it can be used for proofs? http://docs.idris-lang.org/en/latest/tutorial/theorems.html http://docs.idris-lang.org/en/latest/tutorial/theorems.html