Yes, and ACL2 also has proof by reflection. -Ian ----- Original Message ----- From: "John Clements" <cleme...@brinckerhoff.org> To: "Carl Eastlund" <c...@ccs.neu.edu> Cc: "users@racket-lang.org list" <users@racket-lang.org>, "Matthias Felleisen" <matth...@ccs.neu.edu> Sent: Thursday, September 20, 2012 6:40:56 PM GMT -05:00 US/Canada Eastern Subject: Re: [racket] I love TR
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 ____________________ Racket Users list: http://lists.racket-lang.org/users ____________________ Racket Users list: http://lists.racket-lang.org/users
