From 8839959fd05a04f2d37461ab842d23107b104d20 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Fri, 1 May 2026 10:56:10 +0100
Subject: add monotic counters, fix element binding case in app->for

---
 src/checker.rs           |  1 -
 src/checker_signature.rs |  9 +--------
 src/checker_state.rs     | 23 +++++++++++++++--------
 src/main.rs              |  3 +++
 4 files changed, 19 insertions(+), 17 deletions(-)

diff --git a/src/checker.rs b/src/checker.rs
index adb5012..fdba181 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -16,7 +16,6 @@ impl CheckerState {
         let Programme(decls) = prog;
 
         for decl in decls {
-            debug!(%self, %decl);
             match decl {
                 Decl::Set { name, set } => {
                     self.assert_unbound_set(name)?;
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 17154dd..bad38eb 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -1,5 +1,3 @@
-// Time-stamp: <2026-04-30 17h19 BST (9561bc0c)>
-
 use crate::ast::*;
 use crate::checker_state::*;
 use std::collections::HashMap;
@@ -443,12 +441,7 @@ impl CheckerState {
                         let mut ctx = self.clone();
                         let first_set = ctx.check_set(&params[0].set)?;
                         let element_checked = self.check_element(element, &first_set)?;
-                        ctx.make_element_definition(
-                            params[0].name.clone(),
-                            element_checked,
-                            first_set,
-                        )?;
-
+                        ctx.add_element(params[0].name.clone(), element_checked.into(), first_set)?;
                         if params.len() == 1 {
                             ctx.check_instance(body, signature)
                         } else {
diff --git a/src/checker_state.rs b/src/checker_state.rs
index a0fe6b1..3d933f2 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -1,9 +1,12 @@
 use crate::ast::*;
-use tracing::instrument;
 
 use derive_more::Display;
+use tracing::instrument;
+
 use std::collections::HashMap;
 use std::fmt;
+use std::sync::Arc;
+use std::sync::atomic::{AtomicUsize, Ordering};
 
 #[derive(Display)]
 pub enum CheckerError {
@@ -115,9 +118,8 @@ pub struct CheckerState {
     record_fields: HashMap<String, Field<Set>>,
     variant_fields: HashMap<String, Field<Set>>,
     signature_fields: HashMap<String, Field<Signature>>,
-    // TODO: do we need to make these strictly monotonic somewhere somehow?
-    binder_element: usize,
-    unique_name: usize,
+    binder_element: Arc<AtomicUsize>,
+    unique_name: Arc<AtomicUsize>,
 }
 
 impl fmt::Display for CheckerState {
@@ -427,11 +429,16 @@ impl CheckerState {
 
 // -----------------------------------------------------------------------------
 // Bindings
+
+fn _reserved_name(n: usize) -> String {
+    format!("#{}", n)
+}
+
 impl CheckerState {
     fn _make_canonical_element(&mut self, name: String, set: Set) -> Result<String, CheckerError> {
-        let canonical = format!("_#{}", self.binder_element);
+        let n = self.binder_element.fetch_add(1, Ordering::Relaxed);
+        let canonical = _reserved_name(n);
         self.add_element(name, Element::Var(canonical.clone()).into(), set)?;
-        self.binder_element += 1;
         Ok(canonical)
     }
 
@@ -456,7 +463,7 @@ impl CheckerState {
 
     #[instrument(skip(self))]
     pub fn make_unique_name(&mut self) -> String {
-        self.unique_name += 1;
-        format!("_#{}", self.unique_name)
+        let n = self.unique_name.fetch_add(1, Ordering::Relaxed);
+        _reserved_name(n)
     }
 }
diff --git a/src/main.rs b/src/main.rs
index a395db8..eb16b32 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -35,6 +35,9 @@ let set NatEdges = record {
   target: set-of(natGraph .Node),
   connected: set-of(natGraph .Edge source target)
 }
+
+let element s_val : FinTwo = zero. {}
+let element edge : set-of(natGraph .Edge s_val ( one. {} )) = true
 "#;
     let programme = parser::debug_parse(src);
 
-- 
cgit v1.3.1