tutorial-code
tutorial-code copied to clipboard
arend-lang
Source code & exercises in Arend's documentation
In Propositions and sets/Mere Proposition, there is the [following example](https://arend-lang.github.io/documentation/tutorial/PartII/hprops#mere-propositions): ``` \func Unit-isProp : isProp Unit => \lam x y => idp ``` which is rejected with ``` [ERROR] Intro.ard:543:48:...
[There is Exercise 5 in the "Propositions and sets" section](https://arend-lang.github.io/documentation/tutorial/PartII/hprops#mere-propositions): ``` Exercise 5: Prove that \Sigma (x : A) (B x) preserves propositions. ``` But the logic of propositions is...
[The tutorial says](https://arend-lang.github.io/documentation/tutorial/PartI/synndef#namespaces-and-modules) ``` Each definition can be accompanied by \where block in the end. In contrast to Haskell, \where block is attached to the whole definition, not to a...
[This part of the tutorial](https://arend-lang.github.io/documentation/tutorial/PartI/synndef#polymorphism) explains Pi-types basically. There is a basic example of Pi type `\Pi (b : Bool) -> if b Nat Bool`. Most of the examples in...
To be able show that the `StateMonad` is a monad, you need to be able to prove equality of two instances of classes. Even I only know that this can...
When a problem is formulated about `gcd` or matrices, it would be nice to explain the reader how he could check their answer. The students whom I assigned solving these...
It would be nice to explain how the user can connect `arend-lib` to the tutorial code. Explain in accessible way the format of a `arend.yaml` files. What is the difference...
It would be nice to include some material about the very basics of tactics in the tutorial. For example, rewrite/rewriteI/at/I/unfold/ext. Their absence leads to too much verbosity when solving exercises,...
To be able solve one of the exercises in 6th lesson (namely the exercise about `Maybe` monad), you need to know what a dependent `\case` is, and this is explained...
The `+-comm` in `EqualityProofs` must have arguments `n` `m` implicit (because that's the standard pattern actually used in `arend-lib` and everywhere else in the tutorial). Maybe you need to explain...
Metadata
Owner
Metadata
Source code & exercises in Arend's documentation