Library mathcomp.ssreflect.ssreflect
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From Coq Require Export ssreflect.
Distributed under the terms of CeCILL-B. *)
From Coq Require Export ssreflect.
Local additions:
[elaborate x] == triggers coq elaboration to fill the holes of the term x
The main use case is to trigger typeclass inference in
the body of a ssreflect have := [elaborate body].
Intro pattern ltac views:
- calling rewrite from an intro pattern, use with parsimony => / [1! rules] := rewrite rules => / [! rules] := rewrite !rules
Reserved Notation "[ 'elaborate' x ]" (at level 0).
Module Deprecation.
Definition (T : Type) := T.
Definition exposed (T : Type) & unit → unit → unit := T.
Definition hide T u (v : exposed T u) : hidden T := v.
Ltac warn old_id new_id :=
idtac "Warning:" old_id "is deprecated; use" new_id "instead".
Ltac stop old_id new_id :=
fail 1 "Error:" old_id "is deprecated; use" new_id "instead".
Structure hinted := Hint {statement; hint : statement}.
Ltac check cond := let test := constr:(hint _ : cond) in idtac.
Variant reject := Reject.
Definition reject_hint := Hint reject Reject.
Module Reject. Canonical reject_hint. End Reject.
Variant silent := Silent.
Definition silent_hint := Hint silent Silent.
Module Silent. Canonical silent_hint. End Silent.
Ltac flag old_id new_id :=
first [check reject; stop old_id new_id | check silent | warn old_id new_id].
Module Exports.
Arguments hide {T} u v /.
Coercion hide : exposed >-> hidden.
#[deprecated(since="mathcomp 1.13.0",
note="Use the deprecated attribute instead.")]
Notation deprecate old_id new_id :=
(hide (fun old_id new_id ⇒ ltac:(flag old_id new_id; exact tt)) new_id)
(only parsing).
End Exports.
End Deprecation.
Export Deprecation.Exports.
Notation "[ 'elaborate' x ]" := (ltac:(refine x)) (only parsing).
Module Export ipat.
Notation "'[' '1' '!' rules ']'" := (ltac:(rewrite rules))
(at level 0, rules at level 200, only parsing) : ssripat_scope.
Notation "'[' '!' rules ']'" := (ltac:(rewrite !rules))
(at level 0, rules at level 200, only parsing) : ssripat_scope.
End ipat.
A class to trigger reduction by rewriting.
Usage: rewrite [pattern]vm_compute.
Alternatively one may redefine a lemma as in algebra/rat.v :
Lemma rat_vm_compute n (x : rat) : vm_compute_eq n%:Q x -> n%:Q = x.
Proof. exact. Qed.
Class vm_compute_eq {T : Type} (x y : T) := vm_compute : x = y.
Hint Extern 0 (@vm_compute_eq _ _ _) ⇒
vm_compute; reflexivity : typeclass_instances.