search

agda / agda-web-semantic

Agda libraries for the semantic web
MIT License
23 stars 3 forks source link

Usolved Metas #4

Open bblfish opened 3 years ago

bblfish commented 3 years ago

I get the following error message. 

/Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Wiring.agda:19,1-58
Unsolved metas at the following locations:
  /Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Tensor.agda:69,27-35
  /Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Tensor.agda:70,12-20
  /Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Tensor.agda:73,27-35
  /Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Tensor.agda:74,12-20
when scope checking the declaration
  open import Web.Semantic.DL.Category.Tensor using (_⊗_)

Am looking to fix it. I will create a commit referencing this issue when I do.

bblfish commented 3 years ago

After working on a few files that error message disappeared but I still get it another file src/Web/Semantic/DL/Category.agda

Error
/Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category.agda:4,1-44
Unsolved metas at the following locations:
  /Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Composition.agda:99,9-17
  /Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Composition.agda:99,35-43
  /Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Composition.agda:105,9-17
  /Volumes/Dev/Programming/Proof/Agda/agda-web-semantic/src/Web/Semantic/DL/Category/Composition.agda:105,36-44
when scope checking the declaration
  import Web.Semantic.DL.Category.Composition
bblfish commented 3 years ago

This commit deals with the "Unsolved Metas" problem https://github.com/bblfish/agda-web-semantic/commit/064ed896b3559d5d369ac807216a6e324911d5b4

There seem to be a few more problems to get a full clean compile.