Library Mtac2Tests.test_get_reference

From Mtac2 Require Import Mtac2.

Goal forall x, 0 <= x.
MProof.
  H <- M.get_reference "le_0_n";
  dcase H as e in
  T.apply e.
Qed.

Goal forall x, 0 <= x.
MProof.
  H <- M.get_reference "Peano.le_0_n";
  dcase H as e in
  T.exact e.
Qed.

Goal forall x, 0 <= x.
MProof.
  H <- M.get_reference "Coq.Init.Peano.le_0_n";
  dcase H as e in T.apply e.
Qed.

Definition myle0n := le_0_n.

Goal forall x, 0 <= x.
MProof.
  H <- M.get_reference "myle0n";
  dcase H as e in T.apply e.
Qed.

Goal forall x, 0 <= x -> 0 <= x.
MProof.
  intros x H.
  mtry
    H <- M.get_reference "H";
    dcase H as e in T.apply e
  with RefNotFound "H" => T.apply myle0n
  end.
Qed.