| Sometimes we want to create "proofs" that is dependent other other data or other systems - for example a API backend. We can use a "Context" to describe under which scenario the proof holds. Note, there is value to describe the context even if other proofs is not used.
For example:
```cozyAnimals : ForVersionOf BackendResponse (Proved (List CozyAnimals) NonEmptyList)```
Would mean that for a given backendresponse we have proved that the list of cozy animals is non empty
In a different part of the code we could have this type:
```animal : ForVersionOf BackendResponse (Proved Animal CozyAnimal)```
Which would mean that for a given backend response we have proved that the animal in question is a cozy animal
Then in a third part of the code we have both the cozyAnimals and the animal value
To see if the proofs are based on the same backend response we would
```elm
firstCheck : Maybe (ForVersionOf BackendResponse (Proved (List CozyAnimals) NonEmptyList, Proved Animal CozyAnimal)
firstCheck = proveSameVersion cozyAnimals animal
-- Continue here, deciding what to do if the proofs came from two different API responses
```A specialized case of `Context` that is used with `ForVersionOf`.
The `key` is used to ensure that only the correct module/library can create contexts. Extract the version for comparisionCompare two contexts for equalityForget the version, analogous to exorcise for proofs.Put a proof into a contextGet a new version.
If you are interested of the acutal value then you should use `Context` and `For`Get a initial version.
If you are interested of the acutal value then you should use `Context` and `For`Merge two `For`s if they describe values in the same contextContext is more generalized data type that Version is based upon. This is useful if a specific comparable
is prefered or needed instead of just a 'random' number.
For example:
elm
type alias Ears = Int
For AnimalName String (Proven Ears Positive)
Which would mean that for a given AnimalName it is proven that that animal has a positive number of ears.
Due to constraints in Elm the type is more verbose than wanted but here is the breakdown ```elm For AnimalName String (Proven Ears Positive)
-- For: is the name for a Contexbased expression
-- AnimalName: is the constructor that is *not* exported by the Animal-module RefinementProofs.to ensure that no one
-- else can create an AnimalName context and rewire the proofs
-- String: is comparable type that is used to compare two contexts, for an id this is most often Int
-- Proven Ears Positive: The actual expression that is in the described context
```Describes a context in which something can be put.
The `key` is used to ensure that only the correct module/library can create contexts.
Remember to keep the constructors private! Describes a context and what is in that context.
The `key` is used to ensure that only the correct module/library can create contexts.
The `comparable` is the value used to check if two contexts describe the same thing
The `a` is the actual value in the context Compare two contexts for equality, if equal they describe the same contextExtract the context for comparisionMerge two `For`s if they describe values in the same contextPut a proof into a contextCreate a context with a specific value, for example an id.