Trigger CI for https://github.com/leanprover/lean4/pull/5474 #126743
Annotations
4 errors
|
test/aesop_cat.lean#L20
could not synthesize default value for field 'w' of 'Foo' using tactics
|
|
test/aesop_cat.lean#L20
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
|
|
test/aesop_cat.lean#L19
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
|
The logs for this run have expired and are no longer available.
Loading