元素属于集合的类型表示法

林一二2023年07月02日 22:03
学Lean

在 Lean 中不说 p∈P，而用 p : P 表示「术语p」的类型是「类型P」。

例如 n : mynat 来表示 n 是一个自然数

元素属于集合的类型表示法