10 lines
648 B
Text
10 lines
648 B
Text
structure_patterns.lean:10:8: error: non-exhaustive match, the following cases are missing:
|
|
_example {a := 0, b := _, c := _}
|
|
structure_patterns.lean:10:0: warning: declaration '[anonymous]' uses sorry
|
|
structure_patterns.lean:13:25: error: invalid occurrence of structure notation source in pattern
|
|
structure_patterns.lean:13:22: error: invalid structure notation source, not a structure
|
|
f
|
|
which has type
|
|
_
|
|
structure_patterns.lean:13:22: error: invalid structure value { ... }, field 'a' was not provided
|
|
structure_patterns.lean:13:8: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
|