Commit ee9baa0d authored by Amin Timany's avatar Amin Timany

Revert "Add notations in fundamental_unary for aesthetics"

This reverts commit b498dbc4.
parent b498dbc4
......@@ -19,9 +19,6 @@ 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 : τ.
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