The Guide feels like AI slop and I don't understand it

I started reading the guide to start understanding the basics of the lanague.

I got stuck even at the basic for loop (recursion): the guide was starting talking about proofs, let bindings (there are no let bindings in the examples), and generally were mixing levels of concepts even when trying to teach the basics.

I have no idea what this is: A let must be inferable: annotate a literal, as in x = {3 : U32}.

Or this:

A U32 has no 1+p pattern, so loop counters are Nats: case 1n+p: hands you a smaller p to recurse on, and a Nat is still a machine word at runtime (a program aborts past 2^48-1). There is no if: a branch is a match on True{} and False{}.


There's no 1+p in the code.

The whole guide looks like it hasn't even been read once by a human.