The Coq mailing list

[Luminous Fennell <mstrlu AT gmx.net>]

> Reserved Notation "E ⊢ e ∷ τ" (at level 70).
> Inductive well_typed : (ℕ → type) → expr → type → Prop :=
> | Rule1: ∀ E n, » 
>                   ─────────────
>                   E ⊢ [n]∷E n
>
> | Rule2: ∀ E e₁ e₂ τ₁ τ₂, » E ⊢ e₁∷τ₁⟹τ₂     E ⊢ e₂∷τ₁ 
>                             ────────────────────────────
>                             E ⊢ (e₁ e₂)∷τ₂
>
> | Rule3: ∀ E n e τ₁ τ₂, » E{n↦τ₁} ⊢ e∷τ₂ 
>                           ────────────────────
>                           E ⊢ (Λ n·e)∷τ₁⟹τ₂
>

These are some slick notations :) This would definitely be sufficient
for sending rules via email. Though I could imagine that it becomes a bit
tedious to layout the spacing by hand all the time.

However, it doesn't really help for TeX output. I will try to use and
elaborate my provisional tool for a month or so and then make it
available somewhere and ask for more feedback (or report back why it/I
failed).

Thanks for the suggestions!

Best regards

Lu