From 37bb9b49f6fd96a5cd9ad97c7de8f2866797941e Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 27 Jul 2024 00:20:48 +0200 Subject: [PATCH] ensure all URLs have hyperlinks --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 1e7f0b2..ab62055 100644 --- a/README.md +++ b/README.md @@ -96,7 +96,7 @@ To build all the examples in `src/`, run `make`. - `auto with foo nocore` with the pseudo-database `nocore` disables the default `core` hint databases and only uses hints from `foo` (and the context). - If you need to apply a theorem to a hypothesis and then immediately destruct the result, there's a concise way to do it without repetition: `apply thm in H as [x H]`, for example, might be used then `thm` produces an existential for a variable named `x`. - If you have a hypothesis `H: a = b` and need `f a = f b`, you can use `apply (f_equal f) in H`. (Strictly speaking this is just using the `f_equal` theorem in the standard library, but it's also very much like the inverse direction for the `f_equal` tactic.) -- If you want to both run Ltac and return a `constr`, you can do so by wrapping the side effect in `let _ := match goal with _ => side_effect_tactic end in ...`. See https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884 for Jason Gross's much more thorough explanation. +- If you want to both run Ltac and return a `constr`, you can do so by wrapping the side effect in `let _ := match goal with _ => side_effect_tactic end in ...`. See for Jason Gross's much more thorough explanation. - If you want `lia` to help with non-linear arithmetic involving division or modulo (or the similar `quot` and `rem`), you can do that for simple cases with `Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.` See [DivMod.v](src/DivMod.v) for an example and the [micromega documentation](https://coq.github.io/doc/master/refman/addendum/micromega.html) the full details. - Coq's `admit` will force you to use `Admitted`. If you want to use Qed, you can instead use `Axiom falso : False. Ltac admit := destruct falso.` This can be useful for debugging Qed errors (say, due to universes) or slow Qeds. @@ -184,7 +184,7 @@ To build all the examples in `src/`, run `make`. - You can use `all: fail "goals remaining".` to assert that a proof is complete. This is useful when you'll use `Admitted.` but want to document (and check in CI) that the proof is complete other than the `admit.` tactics used. - You can also use `Fail idtac.` to assert that a proof is complete, which is shorter than the above but more arcane. - You can use `Fail Fail Qed.` to really assert that a proof is complete, including doing universe checks, but then still be able to `Restart` it. I think this is only useful for illustrating small examples but it's amusing that it works. (The new `Succeed` vernacular in Coq 8.15 is a better replacement, because it preserves error messages on failure.) -- Hints can now be set to global, export, or local. Global (the current default) means the hint applies to any module that transitivity imports this one; export makes the hint visible only if the caller imports this module directly. The behavior will eventually change for hints at the top-level so that they become export instead of global (see https://github.com/coq/coq/pull/13384), so this might be worth understanding now. [HintLocality.v](src/HintLocality.v) walks through what the three levels do. +- Hints can now be set to global, export, or local. Global (the current default) means the hint applies to any module that transitivity imports this one; export makes the hint visible only if the caller imports this module directly. The behavior will eventually change for hints at the top-level so that they become export instead of global (see ), so this might be worth understanding now. [HintLocality.v](src/HintLocality.v) walks through what the three levels do. - The [uniform inheritance condition for coercions is gone](https://github.com/coq/coq/pull/15789) as of March 2022. This condition required that all the implicit arguments of the target of a coercion could be