[Draft] Deeper integration with Agda: foundational work #97
Annotations
9 errors
|
🏗️ Build ALS
Process completed with exit code 1.
|
|
🏗️ Build ALS:
src/Server/Model/Handler.hs#L90
• Could not deduce ‘TCM.PrettyTCM TCM.TCErr’
|
|
🏗️ Build ALS:
src/Server/Model/Handler.hs#L53
• Could not deduce ‘TCM.PrettyTCM TCM.TCErr’
|
|
🏗️ Build ALS:
src/Indexer/Indexer.hs#L565
Not in scope: data constructor ‘A.OverlapPragma’
|
|
🏗️ Build ALS:
src/Indexer/Indexer.hs#L559
Not in scope: data constructor ‘A.InjectiveForInferencePragma’
|
|
🏗️ Build ALS:
src/Indexer/Indexer.hs#L394
Not in scope: data constructor ‘C.LeftLet’
|
|
🏗️ Build ALS:
src/Indexer/Indexer.hs#L305
Not in scope: type constructor or class ‘A.TacticAttribute’
|
|
🏗️ Build ALS:
src/Agda/Syntax/Abstract/More.hs#L10
Module ‘Agda.Syntax.Concrete’ does not export ‘TacticAttribute'’.
|
|
🏗️ Build ALS:
src/Agda/Interaction/Imports/More.hs#L63
Module ‘Agda.TypeChecking.Monad’ does not export ‘checkAndSetOptionsFromPragma’.
|
Loading