History of doc / Examples.md @master git clone https://git.catseye.tc/Maxixe/

• Update various points of the documentation. Chris Pressey 2 years ago
• Merge branch 'logic-syntax-sugar' into develop-0.2 Chris Pressey 2 years ago
• Attempt a proof by contradiction. It doesn't quite work. Chris Pressey 5 years ago
• Rewrite the Equational Reasoning section. Chris Pressey 5 years ago
• Fix the definition of UG in the number theory proofs. Chris Pressey 7 years ago
• Add definition of nonlocal to spec and refactor example proofs. Chris Pressey 7 years ago
• Allow hole in Universal Generalization to be plugged. Chris Pressey 7 years ago
• Fix formatting in Socrates example and illustrate a problem. Chris Pressey 7 years ago
• Sugar also in the rule: `case`...`end` can be omitted if only 1. Chris Pressey 7 years ago
• Syntatic sugar: if only 1 case in block, case/end need not appear. Chris Pressey 7 years ago
• The sum of an odd number and an odd number is an even number. Chris Pressey 7 years ago
• Show that the variable restriction isn't un-overcome-able. Chris Pressey 7 years ago
• Defns of even and odd can now exist a variable with the same name. Chris Pressey 7 years ago
• Try to justify the presence/absence of 'unique' attribute. Chris Pressey 7 years ago
• Implement occurs check during substitution. Chris Pressey 7 years ago
• Enforcing a final rule in a block-case is now optional. Chris Pressey 7 years ago
• Add simple number theory proof as an example. Chris Pressey 7 years ago
• Can generalize a term and UI to a term. Improve error messages. Chris Pressey 7 years ago
• Initial import of Maxixe source (work-in-progress). Chris Pressey 7 years ago