@edwinbrady @darinmorrison can Idris be used as a companion for the HoTT book? So far I'd only heard no.
@PLT_cheater Not easily, because you can’t turn off axiom K. I’d suggest Agda instead. @darinmorrison
-
-
@edwinbrady@darinmorrison How do Idris and Agda compare? My experience with both is somewhat basic but I know provers in general -
@edwinbrady@darinmorrison also, why wouldn't I use Isabelle/HOL?
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.