From a237c97e0c2c019edcfdfa17371059cd9ce975d9 Mon Sep 17 00:00:00 2001 From: tslil Date: Tue, 28 Apr 2026 13:00:17 +0100 Subject: rework checking logic to revolve around "stuck" computations, the meaning of Hypothetical is now reserved for formal bindings --- src/checker.rs | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'src/checker.rs') diff --git a/src/checker.rs b/src/checker.rs index 05ebca2..976b9fb 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -1,5 +1,5 @@ use crate::ast::*; -use crate::checker_state::{CheckerError, CheckerState, ElementValue}; +use crate::checker_state::{CheckerError, CheckerState}; use tracing::{debug, instrument}; @@ -26,12 +26,7 @@ impl CheckerState { Decl::Element { name, element, set } => { let set = self.check_set(set.clone())?; let element = self.check_element(element.clone().into(), &set)?; - if matches!(element, ElementValue::Hypothetical(_)) { - panic!( - "invariant violation: from concrete values at the top level we returned a hypothetical value" - ); - } - self.add_element(name.clone(), element, set) + self.add_element(name.clone(), element.into(), set) } Decl::Signature { name, signature } => { let signature = self.check_signature(signature.clone())?; -- cgit v1.3.1