- Feb 03, 2017
-
-
Robbert Krebbers authored
-
- Jan 31, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This fixes issue #65.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
This approach is originally by Robbert
-
Robbert Krebbers authored
Fix fixes issue #63.
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
Rename: - prefix_of -> prefix and suffix_of -> suffix because that saves keystrokes in lemma names. However, keep the infix notations with l1 `prefix_of` l2 and l1 `suffix_of` l2 because those are easier to read. - change the notation l1 `sublist` l2 into l1 `sublist_of` l2 to be consistent. - rename contains -> submseteq and use the notation ⊆+
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
This patch was created using find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 ' and some minor manual editing
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Also make names more consistent.
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
-
- Dec 09, 2016
-
-
Robbert Krebbers authored
We typically use the _1 and _2 suffix to denote individual directions of a lemmas that is a biimplication.
-
Ralf Jung authored
-
- Dec 08, 2016
-
-
Robbert Krebbers authored
case H; clear H would fail when H is dependent whereas destruct H would succeed on that, but just not clear it.
-
Robbert Krebbers authored
The case tactic is faster than destruct.
-
Robbert Krebbers authored
Example: Goal ¬False → ¬False → ¬False → ¬False → ¬False → ¬False → ¬False → False. Proof. intros. done. (* takes very long *)
-
- Dec 06, 2016
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Dec 05, 2016
-
-
Robbert Krebbers authored
Using this new definition we can express being contractive using a Proper. This has the following advantages: - It makes it easier to state that a function with multiple arguments is contractive (in all or some arguments). - A solve_contractive tactic can be implemented by extending the solve_proper tactic.
-
- Nov 29, 2016
-
-
Robbert Krebbers authored
-
- Nov 24, 2016
-
-
Robbert Krebbers authored
-
- Nov 23, 2016
-
-
Robbert Krebbers authored
-
Ralf Jung authored
Use notation N @⊆ E to avoid ambiguity. Since `nclose : namespace → coPset` is declared as a coercion, the notation `nclose N ⊆ E` was pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked because type checking goes from left to right, and as such would look for an instance `SubsetEq namespace`, which causes the right hand side to be ill-typed. See merge request !24
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Nov 22, 2016
-
-
Robbert Krebbers authored
-
We do this by introducing a type class UpClose with notation ↑. The reason for this change is as follows: since `nclose : namespace → coPset` is declared as a coercion, the notation `nclose N ⊆ E` was pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked because type checking goes from left to right, and as such would look for an instance `SubsetEq namespace`, which causes the right hand side to be ill-typed.
-