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

feat(builtin/basic): add TypeM alias

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-29 13:03:32 -08:00
parent 1b300d3598
commit f8b82d854e
8 changed files with 2 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/builtin/basic.lean
View file

@ -1,5 +1,7 @@
Import macros Import macros
Definition TypeU := (Type U) Definition TypeU := (Type U)
Definition TypeM := (Type M)
Definition SubstP {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b Definition SubstP {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
:= Subst H1 H2. := Subst H1 H2.

BIN
src/builtin/basic.olean
View file

Binary file not shown.

2
tests/lean/cast4.lean
View file

@ -1,8 +1,6 @@
Import cast Import cast
SetOption pp::colors false SetOption pp::colors false
Definition TypeM := (Type M)
Check fun (A A': TypeM) Check fun (A A': TypeM)
(B : A -> TypeM) (B : A -> TypeM)
(B' : A' -> TypeM) (B' : A' -> TypeM)

1
tests/lean/cast4.lean.expected.out
View file

@ -2,7 +2,6 @@
Set: pp::unicode Set: pp::unicode
Imported 'cast' Imported 'cast'
Set: pp::colors Set: pp::colors
Defined: TypeM
λ (A A' : TypeM) λ (A A' : TypeM)
(B : A → TypeM) (B : A → TypeM)
(B' : A' → TypeM) (B' : A' → TypeM)

2
tests/lean/norm_bug1.lean
View file

@ -1,8 +1,6 @@
Import cast Import cast
SetOption pp::colors false SetOption pp::colors false
Definition TypeM := (Type M)
Check fun (A A': TypeM) Check fun (A A': TypeM)
(a : A) (a : A)
(b : A') (b : A')

1
tests/lean/norm_bug1.lean.expected.out
View file

@ -2,7 +2,6 @@
Set: pp::unicode Set: pp::unicode
Imported 'cast' Imported 'cast'
Set: pp::colors Set: pp::colors
Defined: TypeM
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 : λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
λ (A A' : TypeM) λ (A A' : TypeM)

2
tests/lean/type_inf_bug1.lean
View file

@ -1,8 +1,6 @@
Import cast Import cast
SetOption pp::colors false SetOption pp::colors false
Definition TypeM := (Type M)
Check fun (A A': TypeM) Check fun (A A': TypeM)
(a : A) (a : A)
(b : A') (b : A')

1
tests/lean/type_inf_bug1.lean.expected.out
View file

@ -2,7 +2,6 @@
Set: pp::unicode Set: pp::unicode
Imported 'cast' Imported 'cast'
Set: pp::colors Set: pp::colors
Defined: TypeM
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 : λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
λ (A A' : TypeM) λ (A A' : TypeM)