stepchowfun proofs issues

stepchowfun / proofs

My personal repository of formally verified mathematics.

Other

291 stars 12 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Update Coq to v8.19.2

#680 stepchowfun closed 1 week ago
0
Install `pkg-config`, which is apparently needed to install Coq now

#679 stepchowfun closed 1 month ago
0
Remove explicit `export` locality attributes in `Hint` commands now that the default is `export`

#678 stepchowfun closed 4 months ago
0
Update the toastfile

#677 stepchowfun closed 4 months ago
0
Update GitHub Actions to use non-deprecated versions

#676 stepchowfun closed 5 months ago
0
Add a Tagref reference to the code of conduct file

#675 stepchowfun closed 6 months ago
0
Add some file and directory references

#674 stepchowfun closed 6 months ago
0
Update the Ubuntu version in the toastfile to 24.04 LTS

#673 stepchowfun closed 6 months ago
0
Use a lowercase name for a thing that is not a type

#672 stepchowfun closed 6 months ago
0
Remove some unnecessary parentheses

#671 stepchowfun closed 6 months ago
0
Clarify the issue with eta contraction

#670 stepchowfun closed 6 months ago
0
Wordsmith the admissibility graphs README

#669 stepchowfun closed 7 months ago
0
Add some GitHub-flavored formatting to the admissibility graphs README

#668 stepchowfun closed 7 months ago
0
Fix a comment in the eta equivalence development

#667 stepchowfun closed 7 months ago
0
Make the proofs compatible with Coq 8.19.1

#666 stepchowfun closed 7 months ago
0
coq 8.19.1 can't find `Coq.Arith.Gt` on Arch

#665 sp1ff closed 7 months ago
1
Demonstrate eta conversion for records

#664 stepchowfun closed 7 months ago
0
Clarify how eta contraction would break subject reduction in Coq

#663 stepchowfun closed 7 months ago
0
Explain how eta contraction and cumulativity break subject reduction

#662 stepchowfun closed 7 months ago
0
Fix a typo in a comment

#661 stepchowfun closed 7 months ago
0
Add a discussion about eta equivalence

#660 stepchowfun closed 7 months ago
0
Update the opam check to address a warning in the logs

#659 stepchowfun closed 8 months ago
0
Use `set -x` for shell scripts

#658 stepchowfun closed 8 months ago
0
Update the Ubuntu version in the CI configuration to 22.04 LTS

#657 stepchowfun closed 8 months ago
0
Explain the intuitive motivation for encapsulation and sandboxing

#656 stepchowfun closed 9 months ago
0
Define encapsulation and sandboxing

#655 stepchowfun closed 9 months ago
0
Rename one of the tutorial lessons

#654 stepchowfun closed 9 months ago
0
Fix the case of an identifier

#653 stepchowfun closed 9 months ago
0
Prove some lemmas about admissibility graphs

#652 stepchowfun closed 9 months ago
0
Remove a useless theorem

#651 stepchowfun closed 9 months ago
0
Wordsmith the admissibility graph README

#650 stepchowfun closed 9 months ago
0
Reorder a few theorems

#649 stepchowfun closed 9 months ago
0
Formulate and prove the modularity theorem

#648 stepchowfun closed 9 months ago
0
Wordsmith the admissibility graph README

#647 stepchowfun closed 9 months ago
0
Reformulate modularity

#646 stepchowfun closed 9 months ago
0
Add some missing punctuation

#645 stepchowfun closed 9 months ago
0
Prove some modularity theorems

#644 stepchowfun closed 9 months ago
0
Prove some admissibility theorems

#643 stepchowfun closed 9 months ago
0
Update Coq to v8.18.0

#642 stepchowfun closed 9 months ago
0
Fix a typo in a comment

#641 stepchowfun closed 9 months ago
0
Fix some formatting in the admissibility graphs README

#640 stepchowfun closed 9 months ago
0
Formalize modularity

#639 stepchowfun closed 9 months ago
0
Refactor the admissibility graphs development

#638 stepchowfun closed 9 months ago
0
Wordsmith the admissibility graph README

#637 stepchowfun closed 9 months ago
0
Wordsmith the admissibility graph README

#636 stepchowfun closed 9 months ago
0
Wordsmith the admissibility graph README

#635 stepchowfun closed 9 months ago
0
Wordsmith the admissibility graph README

#634 stepchowfun closed 9 months ago
0
Wordsmith the admissibility graph README

#633 stepchowfun closed 9 months ago
0
Formalize the concepts of `protects` and `contains`

#632 stepchowfun closed 9 months ago
0
Wordsmith the admissibility graph README

#631 stepchowfun closed 9 months ago
0