5a24cb5ef7
@Kha `hygienicIntro` is true by default. `hygienicIntro == false` is the Lean3 behavior. If we find `hygienicIntro` too inconvenient in practice, we set the default to false.
21 lines
378 B
Text
21 lines
378 B
Text
---- h1
|
|
10
|
|
---- h2
|
|
3
|
|
10
|
|
0
|
|
---- h3
|
|
10
|
|
30
|
|
4
|
|
---- inv
|
|
10
|
|
match1.lean:82:0: error: type mismatch during dependent match-elimination at pattern variable 'w' with type
|
|
VecPred P Vec.nil
|
|
expected type
|
|
VecPred P tail✝
|
|
[false, true, true]
|
|
match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found
|
|
.(j + j)
|
|
constructor expected
|
|
[false, true, true]
|