Skip to content

Commit

Permalink
Fix comment
Browse files Browse the repository at this point in the history
  • Loading branch information
mietek committed May 7, 2024
1 parent 6d23302 commit 3a76627
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/A201901/Chapter3.agda
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,7 @@ module NumbersAndBooleans-Part1
if₃ : {t₁ t₂ t₃} t₃ ∈ if t₁ then t₂ else t₃


-- As an exercise, we’re going to define structural induction using three methods. First, a direct definition
-- As an exercise, we’re going to define structural induction using two methods. First, a direct definition
-- using pattern matching.

indStruct : {ℓ} {P : Pred Term ℓ} ( t ( s s ∈ t P s) P t) t P t
Expand Down

0 comments on commit 3a76627

Please sign in to comment.