Mercurial > cpdt > repo

comparison src/Equality.v @ 484:5025a401ad9e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Last round of feedback from class at Penn
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 Jan 2013 16:23:26 -0500
parents f38a3af9dd17
children 31258618ef73
comparison
equal deleted inserted replaced
483:582cf453878e 484:5025a401ad9e
727 727
728 Section fhapp'. 728 Section fhapp'.
729 Variable A : Type. 729 Variable A : Type.
730 Variable B : A -> Type. 730 Variable B : A -> Type.
731 731
732 (** This time, the %\%naive theorem statement type-checks. *) 732 (** This time, the %\%naive%{}% theorem statement type-checks. *)
733 733
734 (* EX: Prove [fhapp] associativity using [JMeq]. *) 734 (* EX: Prove [fhapp] associativity using [JMeq]. *)
735 735
736 (* begin thide *) 736 (* begin thide *)
737 Theorem fhapp_assoc' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) 737 Theorem fhapp_assoc' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2)