tutorial-code
tutorial-code copied to clipboard
Incoherence of definitions in tutorial and arend-lib
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 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.