-Axiom: -----------
- x:A |- x:A
-
-Structural Rules:
-
- Γ, x:A, y:B, Δ |- R:C
-Exchange: -------------------------------
- Γ, y:B, x:A, Δ |- R:C
-
- Γ, x:A, x:A |- R:B
-Contraction: --------------------------
- Γ, x:A |- R:B
-
- Γ |- R:B
-Weakening: ---------------------
- Γ, x:A |- R:B [x chosen fresh]
-
-Logical Rules:
+let div (x:int option) (y:int option) =
+ match (x, y) with (None, _) -> None |
+ (_, None) -> None |
+ (_, Some 0) -> None |
+ (Some m, Some n) -> Some (m / n);;
+</pre>