diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.rs | 2 | ||||
| -rw-r--r-- | src/main.rs | 2 | ||||
| -rw-r--r-- | src/parser.rs | 5 |
3 files changed, 5 insertions, 4 deletions
@@ -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); |