20 lines
765 B
Text
20 lines
765 B
Text
Set: pp::colors
|
||
Set: pp::unicode
|
||
Error (line: 4, pos: 15) type mismatch at definition 'a', expected type
|
||
ℤ
|
||
Given type:
|
||
Bool
|
||
Assumed: vector
|
||
Assumed: const
|
||
let a := 10, v1 := const a ⊤, v2 := v1 in v2 : vector Bool 10
|
||
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2
|
||
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10
|
||
Error (line: 31, pos: 26) type mismatch at definition 'v2', expected type
|
||
vector ℤ a
|
||
Given type:
|
||
vector Bool a
|
||
Assumed: foo
|
||
Coercion foo
|
||
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := v1 in v2 : vector ℤ 10
|
||
Set: lean::pp::coercion
|
||
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := foo v1 in v2
|