From 525c4131ed6329017b4738f0b64a1d8f6c1eb164 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 16:50:27 -0700 Subject: [PATCH] eliminate ext_tree_{left,right} keywords --- src/HaskProof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/HaskProof.v b/src/HaskProof.v index 7ae3462..efb9220 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -40,8 +40,8 @@ Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) := Tree ??(LeveledHaskType Γ ★) -> UJudg Γ Δ. Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50). - Notation "'ext_tree_left'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (ctx,,t) s end). - Notation "'ext_tree_right'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (t,,ctx) s end). + Definition ext_tree_left {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end). + Definition ext_tree_right {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end). (* we can turn a UJudg into a Judg by simply internalizing the index *) Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg := -- 1.7.10.4