[POPLmark] Poplmark Digest, Vol 10, Issue 5
Daniel C. Wang
danwang at CS.Princeton.EDU
Thu Jun 1 21:44:32 EDT 2006
Ahh, you've read between the lines.... correctly. :)
1. There isn't a nice "nat" library I could just include.
2.
height_of_subst : ({x : tm} {dx : height x (s z)} height (E1 x) N1)
-> height E2 N2
-> height (E1 E2) NSubst
-> sum N1 N2 N12
-> lt NSubst N12
-> type.
%mode height_of_subst +X1 +X2 -X3 -X4 -X5.
is the Twelfized version of my challenge problem. It takes me a while to convince my self that's
really the theorem I had in my head before I twelfized it.
Anyway, I want to thank everyone for putting in the effort to code this up.
I think all the examples are really great at showing off the "basics" of each system. i.e.
reasoning about naturals, lambda terms, and basic induction on a relation.
As I'm too old fashioned to know how to use a Wiki properly. I'd appreciate it if someone could put
up links to all the solutions on the Wiki.
Dan Licata wrote:
> {stuff deleted}
> Daniel, you mentioned in a previous e-mail that there is a system in
> which you found this task "tedious". Since you haven't made this
> complaint about the Coq/Isabelle/HOL solutions, I wonder if Twelf is the
> system you had in mind. If so, I'm curious as to why.
>
> -Dan
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
More information about the Poplmark
mailing list