mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
Merge branch 'sofia/async-http-body' into sofia/async-http-h1
This commit is contained in:
@@ -162,7 +162,7 @@ instance : Writer Full where
|
||||
instance : Writer Empty where
|
||||
send _ _ _ := throw <| .userError "cannot send"
|
||||
close _ := pure ()
|
||||
isClosed _ := pure false
|
||||
isClosed _ := pure true
|
||||
hasInterest _ := pure false
|
||||
getKnownSize _ := pure (some (.fixed 0))
|
||||
setKnownSize _ _ := pure ()
|
||||
|
||||
@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
|
||||
module
|
||||
|
||||
prelude
|
||||
import Std.Tactic.BVDecide
|
||||
public import Init.Data.String
|
||||
|
||||
@[expose]
|
||||
|
||||
Reference in New Issue
Block a user