Mercurial > cpdt > repo

comparison src/Reflection.v @ 426:5f25705a10ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 18:10:26 -0400
parents d32de711635c
children 17d01e51256c
comparison
equal deleted inserted replaced
425:6ed5ee4845e4 426:5f25705a10ea
360 (** %\vspace{-.15in}% [[ 360 (** %\vspace{-.15in}% [[
361 t1 = 361 t1 =
362 fun a b c d : A => 362 fun a b c d : A =>
363 monoid_reflect (Op (Op (Op (Var a) (Var b)) (Var c)) (Var d)) 363 monoid_reflect (Op (Op (Op (Var a) (Var b)) (Var c)) (Var d))
364 (Op (Op (Var a) (Op (Var b) (Var c))) (Var d)) 364 (Op (Op (Var a) (Op (Var b) (Var c))) (Var d))
365 (refl_equal (a + (b + (c + (d + e))))) 365 (eq_refl (a + (b + (c + (d + e)))))
366 : forall a b c d : A, a + b + c + d = a + (b + c) + d 366 : forall a b c d : A, a + b + c + d = a + (b + c) + d
367 ]] 367 ]]
368 368
369 The proof term contains only restatements of the equality operands in reified form, followed by a use of reflexivity on the shared canonical form. *) 369 The proof term contains only restatements of the equality operands in reified form, followed by a use of reflexivity on the shared canonical form. *)
370 370