Skip to content

Commit

Permalink
fix: typos in C_Proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
pmbittner committed Oct 14, 2024
1 parent 81a5256 commit 5321e01
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Vatras/Tutorial/C_Proofs.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -115,8 +115,8 @@ are parametric in the type of variants in the variant map.
We will reuse `V` here which was defined in the first tutorial
to be a rose tree just as in our paper.
(Try looking it up using your editor, and feel free to
change it if you like 🙂! (Some proofs might break but you
can just replace them by a whole to experiment a bit)).
change the value of `V` if you like 🙂! (Some proofs might break but you
can just replace them by a hole to experiment a bit.))

```agda
open import Vatras.Framework.Properties.Completeness V
Expand Down

0 comments on commit 5321e01

Please sign in to comment.