We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 4cfa26b commit 013def4Copy full SHA for 013def4
src/Lists.lidr
@@ -622,7 +622,7 @@ _Proof_: By induction on `l1`.
622
We must show
623
624
`length ((n :: l1') ++ l2) = length (n :: l1') + length l2)`.
625
-
+
626
This follows directly from the definitions of `length` and `++` together
627
with the induction hypothesis. $\square$
628
@@ -955,7 +955,7 @@ $\square$
955
956
==== Exercise: 1 star (update_neq)
957
958
-> update_neq : (d : PartialMap) -> (x, y : Id ) -> (o : Nat) ->
+> update_neq : (d : PartialMap) -> (x, y : Id) -> (o : Nat) ->
959
> beq_id x y = False ->
960
> find x (update d y o) = find x d
961
> update_neq d x y o prf = ?update_neq_rhs
0 commit comments