deep-foundation / deep-foundation/deep-theory
Add axiom that guarantees that L is always increases
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
Add axiom that guarantees that L is always increases.
```coq
Variable L : Type.
Variable LS : L -> L.
Variable greater : L -> L -> bool.
Axiom LS_increases : forall n : L, greater n (LS n) = true.
```
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.