From 651a67cb568d80e72f8c6a650b985991f4b129d8 Mon Sep 17 00:00:00 2001 From: tslil Date: Wed, 29 Apr 2026 10:56:16 +0100 Subject: fix parser bug, fix beta reduction for setcoerce, disambiguate set coerce in parser --- src/main.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/main.rs') diff --git a/src/main.rs b/src/main.rs index a40eb87..94a9428 100644 --- a/src/main.rs +++ b/src/main.rs @@ -36,7 +36,7 @@ let signature OneSet = theory { F :: Set } let signature T = theory { A :: Set, B :: (x : set-of({ .F = A } .F)) -> Set, - C :: (x : set-of(A)) (b : set-of(B x)) -> Set + C :: (x : set-of(set-of(set-of(A) :: Set) :: Set)) (b : set-of(B x)) -> Set } let signature Graph = theory { @@ -45,8 +45,8 @@ let signature Graph = theory { } let instance natPoset :: Graph = { - .Node = Nat, - .Edge = for (s : Nat) (t : Nat), Bool + .Node = Nat :: Set, + .Edge = for (s : Nat) (t : Nat), Bool :: Set } let element node : set-of(natPoset .Node) = 7 -- cgit v1.3.1