From 31de6d4406fa5663ecdbc1341521a61b86b13783 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Mon, 27 Apr 2026 18:07:06 +0100
Subject: flip to agda-like grammar, sets & signatures do not have dots in
 their fields, but applications of those do as do constructions

---
 src/main.rs | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

(limited to 'src/main.rs')

diff --git a/src/main.rs b/src/main.rs
index 7d04891..491f6d6 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -20,34 +20,34 @@ fn main() {
     let src = r#"
 
 // let X be the set Y, call it Z
-let set X = record { .b : Bool, .n : Nat }
+let set X = record { b : Bool, n : Nat }
 let set Y = X
-let set Z = record { .y : Y }
+let set Z = record { y : Y }
 // make some elements
 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 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 signature Graph = theory {
-    .Node :: Set,
-    .Edge :: (s : Node) (t : Node) -> Set
+    Node :: Set,
+    Edge :: (s : Node) (t : Node) -> Set
 }
 
-// let instance natPoset :: Graph = {
-//     .Node = Nat,
-//     .Edge = for (s : Nat) (t : Nat), Bool
-// }
-//
-// let element node : set-of(natPoset .Node) = 7
-//
-// let set NatEdges = record {
-//   .source: set-of(natPoset .Node),
-//   .target: set-of(natPoset .Node),
-//   .connected set-of(natPoset .Edge source target)
-// }
+let instance natPoset :: Graph = {
+    .Node = Nat,
+    .Edge = for (s : Nat) (t : Nat), Bool
+}
+
+let element node : set-of(natPoset .Node) = 7
+
+let set NatEdges = record {
+  source: set-of(natPoset .Node),
+  target: set-of(natPoset .Node),
+  connected: set-of(natPoset .Edge source target)
+}
 "#;
     let programme = parser::parser::program(src);
 
-- 
cgit v1.3.1