From 52756c50fca23916131346eb47f2fcf3e0c77aef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2014 12:56:36 -0800 Subject: [PATCH] fix(builtin/heq): extensionality axioms Signed-off-by: Leonardo de Moura --- src/builtin/heq.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index b860bbf81..8ed6aa182 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -27,13 +27,13 @@ axiom hcongr {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B f == f' → a == a' → f a == f' a' axiom hfunext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} {f : ∀ x, B x} {f' : ∀ x, B' x} : - A = A' → (∀ x x', f x == f' x') → f == f' + A = A' → (∀ x x', x == x' → f x == f' x') → f == f' axiom hpiext {A A' : TypeH} {B : A → TypeH} {B' : A' → TypeH} : - A = A' → (∀ x x', B x == B' x') → (∀ x, B x) == (∀ x, B' x) + A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) axiom hallext {A A' : TypeH} {B : A → Bool} {B' : A' → Bool} : - A = A' → (∀ x x', B x == B' x') → (∀ x, B x) == (∀ x, B' x) + A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) variable cast {A B : TypeH} : A = B → A → B