From 651a67cb568d80e72f8c6a650b985991f4b129d8 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Wed, 29 Apr 2026 10:56:16 +0100
Subject: fix parser bug, fix beta reduction for setcoerce, disambiguate set
 coerce in parser

---
 src/checker_state.rs | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'src/checker_state.rs')

diff --git a/src/checker_state.rs b/src/checker_state.rs
index dc76a10..b710ac3 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -442,11 +442,9 @@ impl CheckerState {
             Instance::Var(canonical.clone()).into(),
             signature.clone(),
         )?;
-        // And lo, the special case:
-        // TODO: is this correct in the presence of de bruijn?
+        // And lo, the special case, our chosen canonical form
         if signature == Signature::Set {
-            self.add_set(canonical.clone(), SetValue::Hypothetical)?;
-            self.add_set(name, Set::Var(canonical).into())?;
+            self.add_set(name, Set::ClaimedSet(Instance::Var(canonical)).into())?;
         }
 
         self.binder_instance += 1;
-- 
cgit v1.3.1