I'm getting ahead of myself #oplss schedule wise, but I've been solving homework exercises with Coq. Proving assoc/distrib props is awesome!
-
-
Replying to @queertypes
If I can find the time, I want to compare contrast w/ Idris & Agda. Proof scripts are starting to grow on me. apply, rewrite, intros, split
1 reply 0 retweets 1 like -
Replying to @queertypes
@cppcabrera To save you a bit of time,
@edwinbrady comments here, if memory serves: http://typetheorypodcast.com/2014/09/episode-2-edwin-brady-on-idris/ …@typetheorypcast1 reply 0 retweets 1 like -
Replying to @craigstuntz
@craigstuntz @cppcabrera Hopefully there I said that I think tactics are nice for machines, but pattern matching is nicer for humans!1 reply 0 retweets 1 like -
Replying to @edwinbrady
@edwinbrady That aligns with my feelings. My tactical maneuvering in Coq is 65% trial and error atm. :)@craigstuntz1 reply 0 retweets 0 likes
@cppcabrera I see it mostly as a way to find out how to write proof automation later. I admit it is quite fun though :). @craigstuntz
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.