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-libit 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 nis currently built intoArend.Prelude, so it makes sense to additionally explain how to work with current implementation ofFin n. The definition withfzeroandfsuccan 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.Primebut<inArith.Natis a completely different datatype. Probably some renaming or comment is needed.