unmatchable, axiom

README-zh.md

@@ -165,11 +165,44 @@ higher inductive Int : U where
 | neg : (n : N) -> ... 
     when 
     | zero = pos zero
-
 #infer Int -- : U 
 #eval neg zero -- = pos zero
 ```
 
+### 公理
+
+这样定义公理
+
+```haskell
+axiom def lem {A : U} : Either A (A -> Void)
+```
+
+### 不可匹配类型
+
+```haskell
+unmatchable data Interval : U where 
+| i0 : ... 
+| i1 : ...
+
+-- 这没问题
+def reflTrue (i : Interval) : Bool 
+| i = true
+
+-- 这里产生一个错误, 因为试图对 Interval 进行匹配
+def trueToFalse (i : Interval) : Bool
+| i0 = true 
+| i1 = false
+
+-- 但这种定义是可以的, 因为 when 子句不会进行完全性检查
+higher inductive S1 : U where 
+| base : ... 
+| loop : (i : Interval) -> ... 
+    when 
+    | i0 = base 
+    | i1 = base
+```
+
+
 ### 定理证明?
 
 ShiTT 不是一个 PA, 所以这里直接使用了 Type in Type, 并且将来可能考虑不添加终止检查.

README.md

@@ -139,6 +139,39 @@ higher inductive Int : U where
 #eval neg zero -- = pos zero
 ```
 
+### Axiom
+
+Define an axiom like this,
+
+```haskell
+axiom def lem {A : U} : Either A (A -> Void)
+```
+
+### Unmatchable
+
+```haskell
+unmatchable data Interval : U where 
+| i0 : ... 
+| i1 : ...
+
+-- This is ok
+def reflTrue (i : Interval) : Bool 
+| i = true
+
+-- This is an error, when you try to match on Interval
+def trueToFalse (i : Interval) : Bool
+| i0 = true 
+| i1 = false
+
+-- This is ok, since "when clause" won't do those check.
+higher inductive S1 : U where 
+| base : ... 
+| loop : (i : Interval) -> ... 
+    when 
+    | i0 = base 
+    | i1 = base
+```
+
 ## Other Syntax
 
 ### Let Binding