| 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
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 comparision
Compare two contexts for equality
Forget 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 Fors if they describe values in the same context
Context is more generalized data type that Version is based upon. This is useful if a specific v
is prefered or needed instead of just a 'random' number.
For example: type alias Ears = Int type AnimalName = AnimalName String p : For AnimalName (Proven Ears Positive) p = ...
-- 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
-- Proven Ears Positive: The actual expression that is in the described contextWhich would mean that for a specific AnimalName it is proven that that animal has a positive number of ears.
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 contextId 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 context
Extract the context for comparision
Merge two Fors if they describe values in the same context
Put a proof into a context
Create a context with a specific value, for example an id.
Put a proof into a context
Used by library writers to get the context's value
A specialized case of
Forthat covers a lot of the basic cases and is less verbose to work with.The
keyis used to ensure that only the correct module/library can create contexts.The
ais the actual value in the context