[isabelle] Issue with `Simpl` user guide `Fac` example
I wanted to have a look at Simpl. I built it from a local AFP copy. In the
documentation, there is a section titled “User Guide” (I jumped there
nearly immediately). In this section, at “34.3.4 Recursion”, there is a
sample `Fac` imperative function.
If I type exactly what's exemplified there, I get an error about a type
unification failure. I have to change `CALL` into `PROC` in order to make
primrec fac :: "nat ⇒ nat"
where "fac 0 = 1"
| "fac (Suc n) = (Suc n) * (fac n)";
procedures Fac (N :: nat | R :: nat)
"IF ´N = 0 THEN ´R :== 1
ELSE ´R :== PROC Fac(´N - 1);; ´R :== ´N * ´R
If I write `CALL` instead of `PROC` (the user guide really says `CALL`), I
Type unification failed: Clash of types "⦇A_' :: nat,
B_' :: nat, C_' :: nat,
I_' :: nat, M_' :: nat,
N_' :: nat, R_' :: nat,
S_' :: nat, Arr_' :: nat list,
Abr_' :: char list,
_⦈" and "⦇locals :: _ ⇒ _,
… :: _⦈"
Type error in application: incompatible operand type
Operator: locals ::
(??'a, ??'b, ??'c, ??'d) stateSP_scheme
⇒ ??'b ⇒ ??'c
Operand: s :: (??'a, ??'e) XVcgEx.vars_scheme
I feel disturbed. First the documentation seems wrong, and then, the
documentation which was generated by a fresh build, should have failed if
there is an error somewhere. Or am I wrong? Do I have to report this as a
bug to the author?
Also, a question aside: is it mandatory to import `$AFP/Simpl/Simpl`? It
takes long to load for me, near to ten minutes. Is there an alternative
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and