michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/notation): change the precedence of '->'

Browse source 
It should match the precedence of the implication '=>'.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-06 13:23:20 -08:00
parent d79a626523
commit 2ddcc32c1d
14 changed files with 54 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/notation.h
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#pragma once
namespace lean {
constexpr unsigned g_eq_precedence = 50;
constexpr unsigned g_arrow_precedence = 70;
constexpr unsigned g_arrow_precedence = 25;
class frontend;
void init_builtin_notation(frontend & fe);
}

2
tests/lean/cast2.lean
View file

@ -2,7 +2,7 @@ Variable A : Type
Variable B : Type
Variable A' : Type
Variable B' : Type
Axiom H : A -> B = A' -> B'
Axiom H : (A -> B) = (A' -> B')
Variable a : A
Check DomInj H
Theorem BeqB' : B = B' := RanInj H a

4
tests/lean/cast3.lean
View file

@ -4,10 +4,10 @@ Eval cast (Refl A) x
Eval x = (cast (Refl A) x)
Variable b : B
Definition f (x : A) : B := b
Axiom H : A -> B = A' -> B
Axiom H : (A -> B) = (A' -> B)
Variable a' : A'
Eval (cast H f) a'
Axiom H2 : A -> B = A' -> B'
Axiom H2 : (A -> B) = (A' -> B')
Definition g (x : B') : Nat := 0
Eval g ((cast H2 f) a')
Check g ((cast H2 f) a')

12
tests/lean/elab2.lean
View file

@ -6,19 +6,19 @@ Variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A,
Variable R : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
(B a) = (B' (C A A' (D A A' B B' H) a))
Theorem R2 (A A' B B' : Type) (H : A -> B = A' -> B') (a : A) : B = B' := R _ _ _ _ H a
Theorem R2 (A A' B B' : Type) (H : (A -> B) = (A' -> B')) (a : A) : B = B' := R _ _ _ _ H a
Show Environment 1
Theorem R3 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
fun (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1),
Theorem R3 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1),
R _ _ _ _ H a
Theorem R4 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
fun (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : _),
Theorem R4 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : _),
R _ _ _ _ H a
Theorem R5 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
Theorem R5 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun (A1 A2 B1 B2 : Type) (H : _) (a : _),
R _ _ _ _ H a

4
tests/lean/elab2.lean.expected.out
View file

@ -4,9 +4,9 @@
Assumed: D
Assumed: R
Proved: R2
Theorem R2 (A A' B B' : Type) (H : A → B = A' → B') (a : A) : B = B' := R A A' (λ x : A, B) (λ x : A', B') H a
Theorem R2 (A A' B B' : Type) (H : (A → B) = (A' → B')) (a : A) : B = B' := R A A' (λ x : A, B) (λ x : A', B') H a
Proved: R3
Proved: R4
Proved: R5
Theorem R5 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
Theorem R5 (A1 A2 B1 B2 : Type) (H : (A1 → B1) = (A2 → B2)) (a : A1) : B1 = B2 :=
R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

2
tests/lean/elab3.lean
View file

@ -5,7 +5,7 @@ Variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A,
Variable R : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
(B a) = (B' (C A A' (D A A' B B' H) a))
Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun A1 A2 B1 B2 H a,
R _ _ _ _ H a

2
tests/lean/elab3.lean.expected.out
View file

@ -4,5 +4,5 @@
Assumed: D
Assumed: R
Proved: R2
Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
Theorem R2 (A1 A2 B1 B2 : Type) (H : (A1 → B1) = (A2 → B2)) (a : A1) : B1 = B2 :=
R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

2
tests/lean/elab4.lean
View file

@ -5,7 +5,7 @@ Variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x)
Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A) :
(B a) = (B' (C (D H) a))
Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun A1 A2 B1 B2 H a, R H a
Set pp::implicit true

2
tests/lean/elab5.lean
View file

@ -5,7 +5,7 @@ Variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x)
Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A) :
(B a) = (B' (C (D H) a))
Theorem R2 : Pi (A1 A2 B1 B2 : Type), (A1 -> B1 = A2 -> B2) -> A1 -> (B1 = B2) :=
Theorem R2 : Pi (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B2) :=
fun A1 A2 B1 B2 H a, R H a
Set pp::implicit true

14
tests/lean/interactive/t11.lean Normal file
View file

@ -0,0 +1,14 @@
(**
auto = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
**)
Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _,
lemma2 : B := _,
conclusion : B /\ A := _
in conclusion.
apply auto. done.
apply auto. done.
apply auto. done.

17
tests/lean/interactive/t11.lean.expected.out Normal file
View file

@ -0,0 +1,17 @@
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
# Set: pp::colors
Set: pp::unicode
Proof state:
A : Bool, B : Bool, assumption : A ∧ B ⊢ A
## Proof state:
no goals
## Proof state:
A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A ⊢ B
## Proof state:
no goals
## Proof state:
A : Bool, B : Bool, assumption : A ∧ B, lemma1 : A, lemma2 : B ⊢ B ∧ A
## Proof state:
no goals
## Proved: T2
#

10
tests/lean/tst1.lean.expected.out
View file

@ -13,7 +13,7 @@
Defined: select
Defined: map
Axiom two_lt_three : two < three
Definition vector (A : Type) (n : N) : Type := Π (i : N), (i < n) → A
Definition vector (A : Type) (n : N) : Type := Π (i : N), i < n → A
Definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d
Definition const::explicit (A : Type) (n : N) (d : A) : vector A n := const n d
Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n :=
@ -30,7 +30,7 @@ if (two == two) ⊤ ⊥
update (const three ⊥) two ⊤ : vector Bool three
--------
select::explicit : Π (A : Type) (n : N) (v : vector A n) (i : N), (i < n) → A
select::explicit : Π (A : Type) (n : N) (v : vector A n) (i : N), i < n → A
map type --->
map::explicit : Π (A B C : Type) (n : N), (A → B → C) → (vector A n) → (vector B n) → (vector C n)
@ -39,11 +39,11 @@ map normal form -->
λ (A B C : Type)
(n : N)
(f : A → B → C)
(v1 : Π (i : N), (i < n) → A)
(v2 : Π (i : N), (i < n) → B)
(v1 : Π (i : N), i < n → A)
(v2 : Π (i : N), i < n → B)
(i : N)
(H : i < n),
f (v1 i H) (v2 i H)
update normal form -->
λ (A : Type) (n : N) (v : Π (i : N), (i < n) → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H)
λ (A : Type) (n : N) (v : Π (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H)

2
tests/lean/tst11.lean.expected.out
View file

@ -6,7 +6,7 @@
⊤
Assumed: a
a ⊕ a ⊕ a
Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a == b) → (P b)
Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → a == b → (P b)
Proved: EM2
EM2 : Π a : Bool, a ∨ ¬ a
EM2 a : a ∨ ¬ a

2
tests/lean/tst4.lean.expected.out
View file

@ -11,7 +11,7 @@ f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
EqNice::explicit N n1 n2
f::explicit N n1 n2 : N
Congr::explicit :
Π (A : Type U) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), (f == g) → (a == b) → ((f a) == (g b))
Π (A : Type U) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), f == g → a == b → (f a) == (g b)
f::explicit N n1 n2
Assumed: a
Assumed: b