Skip to content

Commit

Permalink
update to stdlib-v2.0
Browse files Browse the repository at this point in the history
  • Loading branch information
jamesmckinna authored and andreasabel committed Jan 1, 2024
1 parent ea16c4c commit 5d25cf8
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions doc/user-manual/language/with-abstraction.lagda.rst
Original file line number Diff line number Diff line change
Expand Up @@ -676,8 +676,8 @@ This version of ``case_of_`` only works for non-dependent functions. For
dependent functions the target type will in most cases not be inferrable, but
you can use a variant with an explicit ``B`` for this case::

case_return_of_ : ∀ {a b} {A : Set a} (x : A) (B : A → Set b) → (∀ x → B x) → B x
case x return B of f = f x
case_returning_of_ : ∀ {a b} {A : Set a} (x : A) (B : A → Set b) → (∀ x → B x) → B x
case x returning B of f = f x

The dependent version will let you generalise over the scrutinee, just like a
with-abstraction, but you have to do it manually. Two things that it will not let you do is
Expand Down

0 comments on commit 5d25cf8

Please sign in to comment.