deep-foundation / deep-foundation/deep-theory
Make L type generic
Open
enhancement
- Dominant language
- Coq
- Stars
- 3
- Forks
- 3
- PR merge metrics
- No merged PRs in 30d
Description
https://github.com/linksplatform/Theory/blob/19c09c5185ab7fcd80a40cfd9f724082e7c52777/associative_proofs/net_defs.v#L24-L26
Should be transformed into:
```coq
Inductive L (X:Type) : Type :=
| L0: L X
| LS: L X -> L X.
```
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.