ACL2 newbie

I'm learning ACL2: after spending a day understanding what most people feel when they try to program a computer (why the *#@* doesn't it accept my program?), I seem to have a breakthrough that at least allows me to write some functions and make a little progress. Mostly this involves learning "The Method", and becoming a lot more sensitive to all those nagging little corner cases that don't normally ever happen. But of course, the proof system doesn't know they can't happen..

I've gotten it to accept a dozen or so functions, which for me was non-trivial. I'm having trouble now because I need to define a custom :measure on my last function, and I don't understand enough about how ACL2 does rationals (rationalp, natp, numberp, o-p, o<, etc). I assume it will make sense if I read the doc...

It's fun, in a strange way, to be a newbie... I started programming so long ago I have forgotten what it is like to not know how. But ACL2 is letting me remember!