Mercurial > cpdt > repo
comparison src/Reflection.v @ 426:5f25705a10ea
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 |