From fe2e85d71dbeb4a1ceae462e38cd29b29df0f3f7 Mon Sep 17 00:00:00 2001 From: jihgfee <jihgfee@gmail.com> Date: Fri, 29 May 2020 13:37:11 +0200 Subject: [PATCH] Nit --- theories/logrel/term_typing_rules.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v index acf6978..8c98ea0 100644 --- a/theories/logrel/term_typing_rules.v +++ b/theories/logrel/term_typing_rules.v @@ -60,7 +60,7 @@ Section properties. Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed. Lemma ltyped_bool Γ (b : bool) : ⊢ Γ ⊨ #b : lty_bool. Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed. - Lemma ltyped_nat Γ (n : Z) : ⊢ Γ ⊨ #n : lty_int. + Lemma ltyped_int Γ (i : Z) : ⊢ Γ ⊨ #i : lty_int. Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed. (** Arrow properties *) -- GitLab