chore: import Aesop.Frontend when declaring aesop rule sets (#35165)
#21541
mathlib-bors[bot]bors.yml
on: push
ci (staging)
/
Build
18m 12s
ci (staging)
/
Lint style
2m 23s
ci (staging)
/
Post-CI job
Annotations
20 errors
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) declaration type mismatch, 'Prod.Lex.toLex_mono' has type
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) declaration type mismatch, 'Prod.Lex.monotone_fst_ofLex' has type
|
|
ci (staging) / Build
(kernel) declaration has metavariables 'Prod.Lex.instPreorder'
|
|
ci (staging) / Build
Tactic `Aesop.Frontend.Parser.aesopTactic` has not been implemented
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) declaration type mismatch, 'Prod.Lex.toLex_mono' has type
|
|
ci (staging) / Build
(kernel) application type mismatch
|
|
ci (staging) / Build
(kernel) declaration type mismatch, 'Prod.Lex.monotone_fst_ofLex' has type
|
|
ci (staging) / Build
(kernel) declaration has metavariables 'Prod.Lex.instPreorder'
|
|
ci (staging) / Build
Tactic `Aesop.Frontend.Parser.aesopTactic` has not been implemented
|