Meaning of ↑ and define

Open jzhang113 opened this issue 6 years ago • 1 comments

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.

Apr 15 '19 05:04 jzhang113

↑ is the successor function, which increments a natural number. It's a constructor for the natural number ADT defined here https://github.com/clark800/lambda-zero/blob/491e96ad8978793904bea7ef1ab424b5b0fc1353/libraries/prelude.zero#L62

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

Apr 15 '19 16:04 clark800