]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/lib/share.ml
- alpha conversion check added to the brg kernel (succeeds 1/4 of the times)
[helm.git] / helm / software / lambda-delta / lib / share.ml
index c8097d568eac398c663e5ac5a11d7be212bd4cda..600ae9d858a2e4b406fbb50be6445e418e184494 100644 (file)
@@ -17,3 +17,5 @@ let sh1 a1 a2 b1 b2 =
 
 let sh2 a1 a2 b1 b2 c1 c2 =
    if a1 == a2 && b1 == b2 then c1 else c2 (sh a1 a2) (sh b1 b2)
+
+let eq a b = (a == b) || (a = b)