Some definitions given in the tutorial have differently defined counterparts with the same name from arend-lib.
in the tutorial || is the non-truncated definition, but in arend-lib it is truncated, so it can not be used for pattern-matching in the same fashion due to homotopy level checking. Probably Set/Prop variations of basic operators such as && or || should be given names in a similar fashion to Coq/Ssreflect (see any of their tutorials).
Fin n is currently built into Arend.Prelude, so it makes sense to additionally explain how to work with current implementation of Fin n. The definition with fzero and fsuc can be left in the tutorial for illustrative purposes, but probably should be renamed and supplied with a commentary.
< in tutorial is a boolean function similar to an auxiliary function Arith.Prime but < in Arith.Nat is a completely different datatype. Probably some renaming or comment is needed.
Some definitions given in the tutorial have differently defined counterparts with the same name from
arend-lib
.||
is the non-truncated definition, but inarend-lib
it is truncated, so it can not be used for pattern-matching in the same fashion due to homotopy level checking. Probably Set/Prop variations of basic operators such as&&
or||
should be given names in a similar fashion to Coq/Ssreflect (see any of their tutorials).Fin n
is currently built intoArend.Prelude
, so it makes sense to additionally explain how to work with current implementation ofFin n
. The definition withfzero
andfsuc
can be left in the tutorial for illustrative purposes, but probably should be renamed and supplied with a commentary.<
in tutorial is a boolean function similar to an auxiliary functionArith.Prime
but<
inArith.Nat
is a completely different datatype. Probably some renaming or comment is needed.