From c5ebf74c917b94c8499fa5cd2e125b04ec7529b4 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Mon, 27 Apr 2026 15:49:54 +0100
Subject: prepare for more work on signatures, in particular this means
 processing records in telescoped contexts

rework ElementValue, CheckedElement to be type aliases for the generic version over Term : Type
---
 src/checker_signature.rs | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'src/checker_signature.rs')

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 4fa723f..4d5f02c 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -12,14 +12,20 @@ impl CheckerState {
                 let deref = self.lookup_signature(&v)?;
                 Ok(deref.clone())
             }
-            Signature::Ext { params, codomain } => Err(CheckerError::Unimplemented(
+            Signature::Ext { .. } => Err(CheckerError::Unimplemented(
                 "extension signatures".to_string(),
             )),
             Signature::Theory(fields) => {
+                let mut ctx = self.clone();
                 let fields = fields
                     .into_iter()
                     .map(|SigField { signature, name }| {
-                        let signature = self.check_signature(signature)?;
+                        let signature = ctx.check_signature(signature)?;
+                        ctx.add_instance(
+                            name.clone(),
+                            InstanceValue::Hypothetical(signature.clone()),
+                            signature.clone(),
+                        )?;
                         Ok(SigField { name, signature })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
-- 
cgit v1.3.1