-Axiom: -----------
- x:A |- x:A
-
-Structural Rules:
-
-Exchange: Γ, x:A, y:B, Δ |- R:C
- --------------------------------------
- Γ, y:B, x:A, Δ |- R:C
-
-Contraction: Γ, x:A, x:A |- R:B
- --------------------------
- Γ, x:A |- R:B
-
-Weakening: Γ |- R:B
- ---------------------
- Γ, 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>