Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 24 lines (21 sloc) 0.897 kB
7dcc217 Start concentrating on proving reachable states for your resource, an…
Larry Diehl authored
1 module Lemmachine.Default.Proofs where
2 open import Lemmachine
3 import Lemmachine.Default
4 import Lemmachine.Lemmas
5 open import Lemmachine.Default.Lemmas
6 open Lemmachine.Lemmas Lemmachine.Default.resource
7 open import Relation.Binary.PropositionalEquality
8 open import Data.Empty
9 open import Data.Maybe
10 open import Data.Product hiding (map)
11 open import Data.Function using (const)
12 open import Data.List.Any
13
14 methodNotAllowed : r method r ∉ allowedMethods r
15 resolveStatus r ≡ MethodNotAllowed
16 methodNotAllowed r p with methodAlwaysKnown r | methodIsntAllowed r p
17 ... | p₂ | p₃ rewrite p₂ | p₃ = refl
18
19 optionsOK : r method r ∈ allowedMethods r
20 method r ≡ OPTIONS
21 resolveStatus r ≡ OK
22 optionsOK r p p₂ with methodAlwaysKnown r | methodIsAllowed r p
23 ... | p₃ | p₄ rewrite p₃ | p₄ | p₂ = refl
Something went wrong with that request. Please try again.