diff options
Diffstat (limited to 'README/Case.agda')
| -rw-r--r-- | README/Case.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/README/Case.agda b/README/Case.agda index e42f55a..229acf8 100644 --- a/README/Case.agda +++ b/README/Case.agda @@ -22,8 +22,8 @@ pred n = case n of λ ; (suc n) → n } -from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just A x -from-just x = case x return From-just _ of λ +from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just x +from-just x = case x return From-just of λ { (just x) → x ; nothing → _ } |