Commit b498dbc4 authored by Amin Timany's avatar Amin Timany

Add notations in fundamental_unary for aesthetics

parent e7055ed7
......@@ -19,6 +19,9 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Local Notation "A –≻ B" := (TArrow A B) (at level 200).
Local Notation "e < n - vs" := (e.[upn n (env_subst vs)]) (at level 200).
Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ Γ e : τ.
Proof.
induction 1; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=".
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment