plutus
plutus copied to clipboard
IntersectMBO
Improve the documentation of Agda files involving basic Normal Type definitions
Describe the feature you'd like
The files involved, the number of lines, and the estimated percentage of documentation completion (0 is no documentation at all, 100 is documentation is completed).
| File | Number of lines | Percentage of documentation |
|---|---|---|
| Type.BetaNormal | 195 | 70% |
| Type.BetaNBE | 160 | 90% |
| Type.BetaNBE.Soundness | 236 | 60% |
| Type.BetaNBE.Completeness | 575 | 60% |
| Type.BetaNBE.Stability | 59 | 80% |
| Type.BetaNBE..RenamingSubstitution | 484 | 60% |
Describe alternatives you've considered
No response
