Skip to content
GitLab
Explore
Sign in
Dan Frumin
ReLoC-v1
Repository
logrel-conc
F_mu_ref_conc
logrel_binary.v
Find file
Blame
History
Permalink
Tweak the logrel notation
· 3f2ae145
Dan Frumin
authored
Aug 21, 2017
Γ ⊧ e1 ≤ e2 : τ now means ∀ Δ, {⊤,⊤;Δ;Γ} ⊧ e1 ≤ e2 : τ
3f2ae145