chore(library/logic/wf): remove unnecessary :max

This commit is contained in:
Leonardo de Moura 2014-11-14 17:37:05 -08:00
parent 0d982cceed
commit 627c7cb531

View file

@ -124,7 +124,7 @@ trans : ∀a b c, tc R a b → tc R b c → tc R a c
namespace tc
context
parameters {A : Type} {R : A → A → Prop}
notation `R⁺`:max := tc R
notation `R⁺` := tc R
definition accessible {z} (ac: acc R z) : acc R⁺ z :=
acc.rec_on ac