The Coq mailing list

[CJ Bell <siegebell AT gmail.com>]

Here is an approach that works because it uses the existing notation
for " { } " and requires prefixing Hoare triples with "|-" (or some
other keyword). Hard to tell if it breaks something, though.


Inductive ht_pred : Set := ht_pred_: nat->ht_pred.
Inductive ht : ht_pred->nat->ht_pred->Prop := .

Delimit Scope htriple with htriple.
Delimit Scope htriple_pred with htriple_pred.
Arguments ht P%htriple_pred c%nat Q%htriple_pred.

Module Notations.
  Notation " { P } " := (ht_pred_ P%nat) : htriple_pred.
  Notation "|-" := ht (no associativity, at level 0) : htriple.
End Notations.

Module TestNotations.
  Import Notations.
  Open Scope htriple.

  (* do existing notations still work? *)
  Record Rat : Set := mkRat {
    top: nat; bottom: nat; Rat_cond: (gt bottom O) }.
  Goal (forall b:bool, { b=true } + { b=false }). destruct b; auto. Qed.
  Goal {a | a<>false}. exists true; intro; discriminate. Qed.

  Goal (forall p, {p}%htriple_pred = ht_pred_ p). reflexivity. Qed.

  Goal (forall p c q,
    |- {p} c {q} <-> ht (ht_pred_ p) c (ht_pred_ q)).
  Proof. split; intros; auto. Qed.

End TestNotations.



-cj