summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs8
1 files changed, 8 insertions, 0 deletions
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 983f3f8..c8be3a3 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,6 +1,7 @@
#![allow(dead_code)]
use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::var::AlphaVar;
+use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::Normalized;
use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
@@ -51,6 +52,13 @@ impl TyExpr {
pub fn to_value(&self) -> Value {
todo!()
}
+
+ pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
+ normalize_tyexpr_whnf(self, env)
+ }
+ pub fn normalize_whnf_noenv(&self) -> Value {
+ normalize_tyexpr_whnf(self, &NzEnv::new())
+ }
}
fn tyexpr_to_expr<'a>(