change the "claimed set" notation to "set-of" so that David isn't confused

4 files changed, 6 insertions, 5 deletions

diff --git a/grammar.txt b/grammar.txt
index 607d759..516a248 100644
--- a/grammar.txt
+++ b/grammar.txt
@@ -13,7 +13,7 @@ set_field         = "." , lower_ident , ":" , set ;
 variant_set       = "variant" , "[" , [ variant_field { "|" , variant_field } ] , "]" ;
 variant_field     = lower_ident , "." , ":" , set ;
 builtin_set       = "Nat" | "Int" | "Float" | "Str" | "Bool" ;
-claimed_set       = "set" , "(" , instance , ")" ;
+claimed_set       = "set-of" , "(" , instance , ")" ;
 
 signature         = "Set" | theory_sig | function_sig | sig_var | "(" , signature , ")" ;
 theory_sig        = "theory" , "{" , [ sig_field { "," , sig_field } ] , "}" ;
diff --git a/src/ast.rs b/src/ast.rs
index f517b37..ecc0940 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -36,7 +36,7 @@ pub enum Set {
     #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
     Variant(Vec<VariantField>),
 
-    #[display("set({_0})")]
+    #[display("set-of({_0})")]
     ClaimedSet(Instance),
 
     #[display("{_0}")]
diff --git a/src/main.rs b/src/main.rs
index c57eef6..984a438 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -46,7 +46,7 @@ let element compute : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2
 //     .Edge = for (s : Nat) (t : Nat), Bool
 // }
 //
-// let element node : set(natPoset .Node) = 7
+// let element node : set-of(natPoset .Node) = 7
 "#;
     let programme = parser::parser::program(src);
 
diff --git a/src/parser.rs b/src/parser.rs
index 958f09d..4599f7e 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -32,6 +32,7 @@ parser! {
         rule kw_of()            = "of"            wb()
         rule kw_for()           = "for"           wb()
         rule kw_set()           = "set"           wb()
+        rule kw_set_of()        = "set-of"        wb()
         rule kw_Set()           = "Set"           wb()
         rule kw_Nat()           = "Nat"           wb()
         rule kw_Int()           = "Int"           wb()
@@ -116,7 +117,7 @@ parser! {
         = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } }
 
         rule claimed_set() -> Instance
-        = kw_set() "(" _ i:instance() _ ")" { i }
+        = kw_set_of() "(" _ i:instance() _ ")" { i }
 
         rule set() -> Set
         = kw_record()  _ "{" fs:(set_field() ** ",") _ "}" { Set::Record(fs) }
@@ -285,7 +286,7 @@ let set Maybe = variant [
                 .Edge = for (s : Nat) (t : Nat), Bool
             }
 
-            let element node : set(natPoset .Node) = 7
+            let element node : set-of(natPoset .Node) = 7
         "#;
 
         debug_parse(src);