X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;fp=src%2FHaskStrongTypes.v;h=24f349bf7e30cff7a66bdb48100bccc538f18a7f;hp=1287b0bc4927031ac9954d784b7bc95329ebf011;hb=57e387249da84dac0f1c5a9411e3900831ce2d81;hpb=a45824c7d03fcf797e22d2919187a7e97fb567cc

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 1287b0b..24f349b 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -199,6 +199,8 @@ Notation "t @@  l" := (@mkLeveledHaskType _ _ t l) (at level 20).
 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
 
+Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end.
+
 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
   match lht with t@@l => t end.