Meaning of ↑ and define

[jzhang113]

What are the semantics of ↑ and define? The tutorial doesn't explain these, but they are used in the prelude.

The tutorial also doesn't talk about ⦊, ∈, or {}, though these seem to have fairly clear semantics.

[clark800]

↑ is the successor function, which increments a natural number. It's a constructor for the natural number ADT defined here

lambda-zero/libraries/prelude.zero

Line 62 in 491e96a

ℕ ⩴ {0, ↑(_ ∈ ℕ)}

define is basically a prefix form of ≔. Unfortunately the readme is very out of date and incomplete currently.