Definitions of core syntax terms are different

[skybrian]

I see several differences in how core syntax terms are defined in the README, JavaScript, and Kind versions of the core syntax. I assume there must be good reasons, but I was wondering if someone could explain them.

• The ref constructor doesn't appear in the README, but it's there in both JavaScript and Kind. There also doesn't seem to be any syntax distinguishing it from an ordinary variable.
• The def constructor appears in the README and JavaScript, but not in Kind.
• The nat, char, and string constructors appear in JavaScript, but not in the README or Kind.

I'm also wondering why the 'all' constructor is named 'all' (why not 'fun') and why there is an 'eras' flag instead of a separate constructor for '%'.

My guess is that these differences correspond to different stages of compilation, but I haven't figured out how compiles work yet.

[skybrian]

To answer one of my questions, all seems to be short for forall.

[rigille]

The ref constructor doesn't appear in the README, but it's there in both JavaScript and Kind. There also doesn't seem to be any syntax distinguishing it from an ordinary variable.

A ref is just a reference to a bound variable. In the formcore expression ((Nat.add +2) +2) the ref is Nat.add.

The def constructor appears in the README and JavaScript, but not in Kind.
The nat, char, and string constructors appear in JavaScript, but not in the README or Kind.

These differences are because Kind.Core isn't used in our compilation pipeline, its purpose is to be a reference implementation and it's not complete yer. What we do instead is to represent core terms as Kind.Terms. That's not safe as I would like but we can aways define Kind.Term.IsCore(t: Kind.Term): Type and prove these terms really are FormCore terms. In short if the two implementations differ the js version is the right one.