https://github.com/agda/agda-base
This is an experimental base library which is supposed to contain functional datastructures and reflection code.
Science Score: 26.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
○CITATION.cff file
-
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
○DOI references
-
○Academic publication links
-
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (6.5%) to scientific vocabulary
Repository
This is an experimental base library which is supposed to contain functional datastructures and reflection code.
Basic Info
- Host: GitHub
- Owner: agda
- License: other
- Language: Agda
- Default Branch: main
- Size: 159 KB
Statistics
- Stars: 11
- Watchers: 7
- Forks: 0
- Open Issues: 1
- Releases: 0
Metadata Files
README.md
status
At his points, this is just a happy heap of code mixed together from the stdlib, stdlib-meta, 1lab (on a branch). The purpose so far, was to figure out how feasible it is to have a common base library. It seems doable, but it is too much work to do right now (certainly for me alone). Things that seem a lot of work: + It essentially means maintaining some (aparantly not so small) part of the stdlib here and cutting it out in a reasonable way. + There is some stuff on top of the stdlib about monads/effects/etc. I don't know how to make a reasonable choice here, that people would accept, since it is not really my area of expertise. + Picking the right way to deal with all the things coming up in reflection code, also seems to be above my current skills/knowledge.
So for know, I (Felix Cherubini) will just look into running 1lab tactics in the cubical library, since this is why I was thinking more seriously about agda-base anyway...
agda-base
This is an experimental base library which is supposed to contain basic things, like basic datatypes and reflection code. It should be reasonable, to factor out another dependency, the agda-primitives, since the 1lab does things differently here. Equality (in the sense of typal/propositional equality) is out of scope (with the possible exception of things like 'primQNameEquality' or for example the inductively defined equality on the naturals).
contributions, comments and suggestions
... are very welcome.
why?
The idea is to have a common denominator for all the different libraries (e.g. stdlib, cubical, 1lab, ...) and start to work against the tragedy, that so much gets implemented again and again, by making the code build on top of basic definitions interchangeable.
Owner
- Name: Agda Github Community
- Login: agda
- Kind: organization
- Website: https://wiki.portal.chalmers.se/agda
- Repositories: 32
- Profile: https://github.com/agda
GitHub Events
Total
- Watch event: 1
Last Year
- Watch event: 1
Issues and Pull Requests
Last synced: about 1 year ago
All Time
- Total issues: 1
- Total pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Total issue authors: 1
- Total pull request authors: 0
- Average comments per issue: 0.0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 0
- Pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Issue authors: 0
- Pull request authors: 0
- Average comments per issue: 0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0