From 3922e24270518be67192ad6928bb839132c74c07 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 23 Sep 2020 17:03:42 +0200
Subject: Basic experiments adding reduction to the type checker

---
 hott/List+.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'hott/List+.thy')

diff --git a/hott/List+.thy b/hott/List+.thy
index b73cc24..869d667 100644
--- a/hott/List+.thy
+++ b/hott/List+.thy
@@ -10,8 +10,8 @@ section \<open>Length\<close>
 definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)"
 
 experiment begin
-  Lemma "len [] \<equiv> ?n" by (subst comp)
-  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp)
+  Lemma "len [] \<equiv> ?n" by (subst comp; typechk?)
+  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp; typechk?)+
 end
 
 
-- 
cgit v1.2.3