Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / stepchowfun/proofs issues and pull requests

#579 - Bring back the proof-by-reflection development

Pull Request - State: closed - Opened by stepchowfun over 1 year ago

#100 - Ensure that magicWith can solve the goal if the provided tactic can

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#99 - Introduce the 'gen' tactic notation

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#98 - Simplify the magicWith tactic

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#97 - Destruct conditionals in hypotheses

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#96 - Automatically destruct 'if' conditions in 'magic'

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#95 - Make a few style fixes

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#94 - Be less specific in a comment

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#93 - Simplify the 'simplify' tactic

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#92 - Smith some words

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#91 - Remove unused imports

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#90 - Introduce the 'clean' tactic

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#89 - Add an 'e' variant of magic and sort hypotheses in simplify

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#88 - Reorganize a couple of tactics

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#87 - Simplfiy some proofs

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#86 - Don't use eauto in magic

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#85 - Improve the magic tactic

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#84 - Add a stylistic line break

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#83 - Use singular module names

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#82 - Add a hint

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#81 - Tweak some style

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#80 - Don't use \/ or /\ in inductive propositions

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#79 - Revert "Prove that a simple grammar is unambiguous"

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#78 - Fix a small bug in the invert tactic

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#77 - Prove that a simple grammar is unambiguous

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#76 - Update a comment

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#75 - Make the 'feed' tactic more magical

Pull Request - State: closed - Opened by stepchowfun over 6 years ago

#74 - Refactor the STLC proofs

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#73 - Remove some redundancy in the comments

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#72 - Update 'make clean' to clean up Coq 8.7 files

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#71 - Rewrite the linter in Ruby

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#70 - Remove some extra full stops

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#69 - Fix another typo

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#68 - Fix a small typo

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#67 - Lint for tabs

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#66 - Make some minor style improvements

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#65 - Implement the 'Name' signature (and rename it to 'NameSig')

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#64 - Make a minor style improvement

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#63 - Make the STLC preservation proof a little more straightforward

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#62 - Add the soundness theorem as a hint

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#61 - Make a slight improvement to the STLC progress proof

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#60 - Replace 'Stlc' with 'STLC'

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#59 - Formalize System F and prove the soundness theorem

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#58 - Introduce a new 'invert' tactic and other improvements

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#57 - Alphabetize universal quantifications

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#55 - Switch from eauto to auto

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#54 - Remove an extra space from the Dockerfile

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#53 - Clarify some comments

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#52 - Remove some unnecessary parentheses and also remove the eq definition

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#51 - Fix some indentation

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#50 - Pin the version of every package

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#49 - Adjust some formatting

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#48 - Adjust some formatting

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#47 - Add Booleans to the STLC development

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#46 - Refactor the STLC proofs

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#45 - Remove another unnecessary rewrite hint

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#44 - Remove an unnecessary rewrite hint

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#43 - Prove facts about initial and terminal objects

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#42 - Formalize initial and terminal objects

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#41 - Remove unnecessary branching in the magic tactic

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#40 - Remove some unnecessary resolve hints

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#37 - Define the opposite category

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#36 - Indent a line in the Makefile

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#35 - Create a user for the Docker image rather than doing the build as root

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#33 - Simplify some more proofs

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#32 - Simplify the Cat proof

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#31 - Simplify some proofs

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#30 - Simplify a few proofs

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#29 - Add a comma between the metavariables for natural transformations

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#28 - Update the README

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#27 - Clarify some comments

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#26 - Prove that categories form a category

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#25 - Use universe polymorphism so we can construct a category of categories

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#24 - Don't use any auto-named variables

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#23 - Use records instead of modules for the category theory development

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#22 - Add more intro content

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#21 - Remove a debugging line from the Makefile

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#20 - Clarify some comments

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#19 - Organize the developments into subdirectories

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#18 - Put the Kleene development in a module

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#17 - Simplify the 'evenness' example

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#16 - Prove that Maybe is a functor and a monad

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#15 - Formalize the definition of monad

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#14 - Formalize whiskering

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#12 - Formalize some operations on functors and natural transformations

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#11 - Formalize some category theory

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#10 - Add a stylistic line break to the Dockerfile

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#9 - Monotone can be increasing or *decreasing*

Issue - State: closed - Opened by innovimax almost 7 years ago - 8 comments

#8 - Add a _CoqProject file

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#7 - Fix the path to the Dockerfile

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#6 - Fix the COQPATHs in the Makefile

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#5 - Make the .gitignore list more robust

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#4 - Sort targets in the Makefile and make the 'clean' target more robust

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago

#2 - Prove the Kleene fixed-point theorem

Pull Request - State: closed - Opened by stepchowfun almost 7 years ago