From 05921a049e31382bc581badd5a0b0bd27473e1fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= Date: Tue, 28 May 2024 15:38:44 +0200 Subject: [PATCH] Rename discr to match paper --- theories/Examples.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Examples.v b/theories/Examples.v index fb6b0da..efb5335 100644 --- a/theories/Examples.v +++ b/theories/Examples.v @@ -337,7 +337,7 @@ Proof. - apply rtyping_triv. Qed. -Definition erased_nat_discr := +Definition discr := lam mGhost (Erased tnat) ( reveal (var 0) (lam mGhost (Erased tnat) (gheq (Erased tnat) (hide tzero) (gS (var 0)) ⇒[ 0 | 0 / mProp | mProp ] bot)) @@ -352,8 +352,8 @@ Definition erased_nat_discr := )) ). -Lemma type_erased_nat_discr : - [] ⊢ erased_nat_discr : +Lemma type_discr : + [] ⊢ discr : Pi 0 0 mProp mGhost (Erased tnat) ( (gheq (Erased tnat) (hide tzero) (gS (var 0))) ⇒[ 0 | 0 / mProp | mProp ] bot