Skip to content
Browse files

Hide isAuthorized under AuthHead shim type around Bool for now

  • Loading branch information...
1 parent 984d552 commit 98d43e2dbeed4d9bd6640d9b4cf9d439f50af4e3 @larrytheliquid committed
Showing with 6 additions and 3 deletions.
  1. +4 −1 Lemmachine/Request.agda
  2. +2 −2 Lemmachine/Resource.agda
View
5 Lemmachine/Request.agda
@@ -1,7 +1,10 @@
module Lemmachine.Request where
+open import Data.Bool
-data Request : Set where
+AuthHead = Bool
data Method : Set where
HEAD GET PUT DELETE POST : Method
TRACE CONNECT OPTIONS : Method
+
+data Request : Set where
View
4 Lemmachine/Resource.agda
@@ -6,7 +6,7 @@ data Resource : Set where
resource :
(resourceExists : Request -> Bool)
(serviceAvailable : Request -> Bool)
- (isAuthorized : Request -> Bool)
+ (isAuthorized : Request -> AuthHead)
(forbidden : Request -> Bool)
-> Resource
@@ -16,7 +16,7 @@ resourceExists _ = true
serviceAvailable : Request -> Bool
serviceAvailable _ = true
-isAuthorized : Request -> Bool
+isAuthorized : Request -> AuthHead
isAuthorized _ = true
forbidden : Request -> Bool

0 comments on commit 98d43e2

Please sign in to comment.
Something went wrong with that request. Please try again.