Formatting text: a number bound by def needs no type

A number bound by def is read as the number written there would be, so
the guide no longer asks for (: n int), and says when (: n double) is
needed.

🤖 Generated with [ECA](https://eca.dev) (anthropic/claude-opus-5-5)

Co-Authored-By: eca-agent <git@eca.dev>

_01.Language-basics.sz

@@ -24,21 +24,20 @@ git pull
 
 @subsection{Your first bjolang program}
 
-Bjolang compiles to c#. Many of the design decisions behind bjolang stems from this limitation. The first one you will encounter is that a program needs a main function. like the one in c#, that returns an int. If execution ended correctly it should return 0 if the program executed successfully. 
+Bjolang compiles to c#. Many of the design decisions behind bjolang stems from this limitation. The first one you will encounter is that a program needs a main function, like the one in c#. An int it returns is the program's exit code, 0 when it ran correctly; a main that returns anything else exits with 0.
 
 @codeblock[#:lang "bjolang"]{
-(: print-hello (-> string unit))
+(: print-hello (-> string void))
 (defun (print-hello name)
   (println (str "Hello, " name "!")))
 
 (defun (main args)
-  (print-hello "User")
+  (print-hello "User"))
-  0)
 }
 
 This can then be run using @code{bjo run filename}, and it should print @code{Hello, User!}. 
 
-What you can see here is that defun is the form for defining a function. main is special, it needs no type declaration. print-hello is a regular function, and thus has to declare its type. Everything at toplevel needs to do that. The form is (: name type). A function type is declared as (-> ArgType ... Return-Type). print-hello takes a string argument and returns unit. unit is the name for nothing.
+What you can see here is that defun is the form for defining a function. main is special, it needs no type declaration. print-hello is a regular function, and thus has to declare its type. Everything at toplevel needs to do that. The form is (: name type). A function type is declared as (-> ArgType ... Return-Type). print-hello takes a string argument and returns void. void is the name for nothing: the unit type, whose one value is what println gives back.
 
 @subsection{Declaring types}
 For most of your bjolang code, you will only declare types in the top level. Types within functions are inferred, so declaring types there is almost never necessary. A value type is declared just like a function, but without the function type declaration:
@@ -62,7 +61,7 @@ You can also declare your own types. Either aliases of other types, records of y
 This can then be destructed using pattern matching.
 
 @codeblock[#:lang "bjolang"]{
-(: print-user (-> User unit))
+(: print-user (-> User void))
 (defun (print-user u)
   (match u
     ;; Subpatterns: here we match name, age, the Card rank
@@ -119,14 +118,14 @@ A function takes any number of arguments and produces a value. The signature of
   ;; the last expression in the body is the return value
   (* x 2))
 
-(:print-n-times (-> string int unit))
+(: print-n-times (-> string int void))
 (defun (print-n-times what n)
   (loop (:for i (up-from 0 #:to n))
-    (println what)))
+    (:do (println what))))
 
 ;; call twice takes a function take takes an argument
-;; of type %a and returns unit. 
+;; of type %a and returns void.
-(: call-twice (-> (-> %a unit) %a unit))
+(: call-twice (-> (-> %a void) %a void))
 (defun (call-twice f val)
   (f val)
   (f val))

_02_.Writing-programs.sz

@@ -627,7 +627,6 @@ So one thing needs no brackets, and several things are a vec:
 
 @codeblock[#:lang "bjolang"]|{
 (def name "Ada")
-(: n int)
 (def n 3)
 
 (show "Hello\n")                                        ;; Hello
@@ -658,7 +657,7 @@ Anything else is converted first:
 
 @code{BStr}, @code{BInt}, @code{BChar} and @code{BMany} are the cases of @code{Block}. You rarely write them, but like any constructor they are functions, so @code{(vec-map BStr names)} is a vec of blocks.
 
-@strong{A number bound by @code{def}.} The @code{(: n int)} above is needed. @code{(def n 3)} alone does not say which kind of number @code{n} is, as it could still become a long or a double, so it cannot be read as a block, and the compiler says so at @code{n}. The same holds for @code{(def xs [1 2 3])} and @code{(def total (+ 1 2))}. A number that comes from a typed parameter, a record field or a function such as @code{vec-length} has its type already, and a number written in the vec itself, as in @code{["n = " 3]}, is an int.
+@strong{A number bound by @code{def}.} @code{(def n 3)} does not say which kind of number @code{n} is: it could still become a long or a double. Where a block is wanted, it is read as the number written there would be, so @code{["n = " n]} is what @code{["n = " 3]} is, and @code{n} is an int from then on. A number that is used as a double later, as in @code{(+ n 0.5)}, needs @code{(: n double)} above its @code{def}.
 
 @strong{Where a block is wanted.} A string or a vec is read as a block where the compiler knows that a block is wanted: as an argument, as what a function declared to return a @code{Block} returns, and as the value of a binding whose type is written, such as @code{(: parts Block)}. A @code{def} without a type is what its value is: @code{(def parts ["a" "b"])} is a @code{(Vec string)}, and @code{(show parts)} is refused. Write @code{(: parts Block)} above it.
 
@@ -928,7 +927,6 @@ The messages for the common mistakes, and what to write instead:
 | Block: ... found the number 1.5                                        | @code{(numeric 1.5)}                                |
 | Block: ... found a boolean, or found a bool                            | @code{(if b "yes" "no")}                            |
 | Block: ... found a (Vec string)                                        | @code{(vec-map BStr xs)}, or @code{(: xs Block)} above @code{(def xs ...)} |
-| Block: 'n' is a number, and nothing says yet whether it is an int ...  | @code{(: n int)} above @code{(def n 3)}             |
 | Block: ... found a (Vec (Vec ...)), at a lambda that returns a vec    | @code{(each [...])} around the vec the lambda returns |
 }
 

_04.Appendices.sz

@@ -67,12 +67,12 @@ When compiled, the frontend rejects this with:
 Type Error: Function 'greet' requires a type signature (: greet ...) at hello.bjo:1:1
 }|
 
-@strong{Why it happens:} Unlike local helper functions defined inside another function, every top-level definition in a module must carry an explicit type signature. The compiler requires this so that module interfaces are self-documenting and can be emitted into the compiled assembly's public metadata without requiring whole-program inference across files. The only exception is @code{main}, which has a fixed signature known to the compiler.
+@strong{Why it happens:} Unlike local helper functions defined inside another function, every top-level definition in a module must carry an explicit type signature. The compiler requires this so that module interfaces are self-documenting and can be emitted into the compiled assembly's public metadata without requiring whole-program inference across files. The only exception is @code{main}: the compiler knows what it takes, the arguments as a @code{(Vec string)}, and what it returns is the exit code when it is an int.
 
 @strong{How to fix it:} Add an explicit signature right before the definition:
 
 @codeblock[#:lang "bjolang"]|{
-(: greet (-> string unit))
+(: greet (-> string void))
 (defun (greet name)
   (println (str "Hello, " name)))
 }|