@edwinbrady youre doing a stellar job if the lack of an interactive mode is the prime complaint!
-
-
-
@larrytheliquid@edwinbrady agreed! As it should be this should not be main concern when designing a language. This can be added easily. - 4 more replies
New conversation -
-
-
@edwinbrady You are well-positioned to receive the crossfire from both the theorem provers, and the audience looking for a big standard lib. -
@a_cowley Indeed. Though we're working on removing the excuses to not like Idris, one by one :).
End of conversation
New conversation -
-
-
@edwinbrady Would be interesting to read an idris vs adga comparison -
@rickasaurus Indeed. Ideally written by an independent observer though! - 1 more reply
New conversation -
-
-
@darinmorrison@edwinbrady there's a start of such a backend already actually - see http://github.com/idris-hackers/idris-mode …Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@darinmorrison@d_christiansen@edwinbrady I've been looking into writing a vim mode for Agda 2.3.2, and no. Sends very explicit commands. -
@carloangiuli@darinmorrison@edwinbrady idris-mode uses an sexp syntax, but it's not elisp. We just like parens better than XML.
End of conversation
New conversation -
-
-
@darinmorrison@edwinbrady wishing for an agda-like interactive emacs mode that was lang-agnostic (for langs that resemble agda/idris) -
@darinmorrison@edwinbrady dunno if implementation differences would make it too hard, but proof general did ok between coq and isabelle
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.