On Sep 20, 2012, at 3:35 PM, Carl Eastlund wrote: > [possibly off-topic] > > Is it weird to anyone else that the dependent type comparison table, as well > as the proof assistant comparison table linked right above it, seem to assume > that proof assistants and dependently typed languages are synonymous? This > assumption, for instance, makes ACL2 look absolutely terrible on the proof > assistant comparison chart. Even after I fixed it up to acknowledge that > yes, ACL2 does have proof automation, thank you very much.
Yes, that struck me as very strange, as well. John Clements
smime.p7s
Description: S/MIME cryptographic signature
____________________ Racket Users list: http://lists.racket-lang.org/users
