@edwinbrady @jonsterling why wouldn’t idris work without tactics?
@psygnisfive Well if you'd prefer to write automatable proofs by hand, that's up to you. We're more ambitious (or, one might say, lazy).
-
-
@edwinbrady as i said, i dont. i want pseudo-tactics like agsy which produce code as output that i can understand if i wanted to -
@edwinbrady i say, if you’re going to do all the work of making the machine write code for you, it’s an awful shame to hide it from you
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.