小编Geo*_*nov的帖子

我什么时候应该更喜欢创建数据类型而不是计算类型？

具体示例 - 给出：

data Zero : Set where

record One : Set where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

想要定义 \lt，它们各自的优点和缺点是什么：

-- a new datatype
data _<_ : Nat -> Nat -> Set where
  ozero : {n : Nat} -> zero < suc n
  osuc : {n m : Nat} -> n < m -> suc n < suc m

与

-- calculating
_<_ : Nat -> Nat -> Set
zero < …

s 代码库中似乎有一些“全局变量”（unsafePerformIO+ NOINLINE）warp。尽管如此，warp从同一个main函数运行两个实例是否安全？