[Renamed Model to the more correct ApplicativeStructure.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080313163645] {
move ./SimplyTyped/Model.agda ./SimplyTyped/ApplicativeStructure.agda
hunk ./Everything.agda 13
--- Models.
+-- Applicative structures.
hunk ./Everything.agda 15
-import SimplyTyped.Model
+import SimplyTyped.ApplicativeStructure
hunk ./SimplyTyped/ApplicativeStructure.agda 2
--- Models
+-- Applicative structures
hunk ./SimplyTyped/ApplicativeStructure.agda 5
--- Note: I don't think I have included all the laws that these
--- structures need to satisfy in order to be models. I should probably
--- have called them "applicative structures" instead.
-
-module SimplyTyped.Model where
+module SimplyTyped.ApplicativeStructure where
hunk ./SimplyTyped/ApplicativeStructure.agda 9
--- A simple kind of model.
-
-record Model : Set1 where
+record ApplicativeStructure : Set1 where
hunk ./SimplyTyped/Evaluation.agda 14
-open import SimplyTyped.Model
+open import SimplyTyped.ApplicativeStructure
hunk ./SimplyTyped/Evaluation.agda 24
--- Model.
+-- Applicative structure.
hunk ./SimplyTyped/Evaluation.agda 26
-model : Model
-model = record
+appStr : ApplicativeStructure
+appStr = record
hunk ./SimplyTyped/Evaluation.agda 36
-  -- The model above may be hard to grasp at first. If the
-  -- interpretation function is written out explicitly we get the
+  -- The applicative structure above may be hard to grasp at first. If
+  -- the interpretation function is written out explicitly we get the
hunk ./SimplyTyped/Normalisation.agda 9
-open import SimplyTyped.Model
+open import SimplyTyped.ApplicativeStructure
hunk ./SimplyTyped/Normalisation.agda 17
-  where open Model valModel
+  where open ApplicativeStructure appStr
hunk ./SimplyTyped/Value.agda 11
-open import SimplyTyped.Model
+open import SimplyTyped.ApplicativeStructure
hunk ./SimplyTyped/Value.agda 73
--- A model using these values.
+-- An applicative structure using these values.
hunk ./SimplyTyped/Value.agda 75
-valModel : Model
-valModel = record
+appStr : ApplicativeStructure
+appStr = record
hunk ./SimplyTyped/Value.agda 85
-  -- The evaluation function that you get from this model:
+  -- The evaluation function that you get from this applicative
+  -- structure:
}