diff options
Diffstat (limited to 'src/main.rs')
| -rw-r--r-- | src/main.rs | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/main.rs b/src/main.rs index 3f6b3cc..a40eb87 100644 --- a/src/main.rs +++ b/src/main.rs @@ -20,16 +20,16 @@ fn main() { let src = r#" // let X be the set Y, call it Z -let set X = record { b : Bool, n : Nat } -let set Y = X -let set Z = record { y : Y } +// let set X = record { b : Bool, n : Nat } +// let set Y = X +// let set Z = record { y : Y } // make some elements -let element x : X = { .b = true, .n = 41 } -let element z : Z = { .y = x } +// let element x : X = { .b = true, .n = 41 } +// let element z : Z = { .y = x } // exercise case matching -let set Z_or_Float = variant [ z : Z | f : Float ] -let element injected : Z_or_Float = z. z -let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ] +// let set Z_or_Float = variant [ z : Z | f : Float ] +// let element injected : Z_or_Float = z. z +// let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ] // this should be difficult unless we correctly handle various forms of alpha/beta let signature OneSet = theory { F :: Set } |