From 67e3285ae6c7b94adc1983dcff18a009455bc582 Mon Sep 17 00:00:00 2001 From: tslil Date: Tue, 28 Apr 2026 15:00:45 +0100 Subject: snapshot of working through instances/singatures <> sets/elements --- src/main.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/main.rs') 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 } -- cgit v1.3.1