pristine:e3efef7da5fe58dd7e9e138c7759b1b7cd47bd9805de48479b195bcbc9c86d27 [A well-typed definition of the simply typed lambda calculus. Nils Anders Danielsson **20080310040028 + Includes a simple semantics and a normaliser which uses NBE. + No proofs, but everything is well-typed and structurally recursive. ] hash: 0000014691-7a5b7c161e193ba4f8a929fef152002a4f9d49352f2f5b2fbae6781ce54a4ee6 [Included an infinite set of base types. Nils Anders Danielsson **20080310040440] hash: 0000001792-502e561c941101a5eb7c4551d672f43aaac480ebe49daf62836ac52973dfb300 [Added a file which imports all the other files. Nils Anders Danielsson **20080310040453] hash: 0000000661-d56c9716cc2232d38d80044be2d4ba4139ea75b894cec2b3588bc1e6bb9504b3 [Added a boring file. Nils Anders Danielsson **20080310040532] hash: 0000000193-4289c87e419c022fca69c3911217f0c9e25715cacf23a7e0aef6fdca01f2eade [Added minor comment. Nils Anders Danielsson **20080310044350] hash: 0000000283-1eb8b4d5e15a3688fc5f408961a29ff9dfb016fc32357f8cca314665456b83bc [Renamed _++_ to _▻▻_. Nils Anders Danielsson **20080310130833] hash: 0000003110-f86f241fd25be13c1c632ccaac78bfde9fc1aa8347ddb767cfe619eb28812cc6 [Failed attempt at removing need for lemma by using Church encoding. Nils Anders Danielsson **20080310234624] hash: 0000003436-df952eb8ea85be040d0c7a81eb772b9988fc6c9bae4c98c6adfc0eb847cb6b84 [Failed attempt at removing need for lemma by using Church encoding. Nils Anders Danielsson *-20080310234624] hash: 0000003436-f1fdf84cb3c35f246df9beabb714ae30bc97f5e4d866d736b562b3462c6224d0 [Renamed Semantics to Evaluation. Nils Anders Danielsson **20080310234919] hash: 0000000442-f4b534dd320355f8d08aea5469da6dc8ad108139bf3688bb2231c380548b090d [Minor cleanup. Nils Anders Danielsson **20080310235006] hash: 0000000529-176d4648850a3fb1d97f23f6a0eac8980a3e6c6a9678b3148f664faaf4a711f5 [Fixed bug in definition of η-long β-normal forms. Nils Anders Danielsson **20080311172848] hash: 0000000455-6506c0b947ace97a727b3c610d6fdc0dfe2abfee8e4eff44fac51374b4ffdfb1 [Listed the files in dependency order, added descriptions. Nils Anders Danielsson **20080311173234] hash: 0000000831-c8fc957f38580e7c1b7d919b85acc7503a6b4bbea3c7147b625f4f045b7d772b [Defined a reduction semantics, along with some lemmas. Nils Anders Danielsson **20080312001247] hash: 0000005536-b4367f08150c60b29bcb5923fcaac3ea9da111eb222d38f57a86e84a890e2881 [Defined varToVal and valToTm. Nils Anders Danielsson **20080312001301] hash: 0000000493-a1b9a18edb124375465ae75ed389b41cf19b45b5e959ba1bb21293dbc0244815 [Simplified code by using Data.Star. Nils Anders Danielsson **20080312005346] hash: 0000002907-edbf4c6afdd93c360f2cc69aefdd2cb395ee3665b4e99069209ea298b6f20b1d [Added _⇛⟨_⟩_ and _⟶⟨_⟩_. Nils Anders Danielsson **20080312133915] hash: 0000000604-8621c0b047abee5e8fb1144bc63f575a853becbd3d0090e6aa2173a1bf41774c [Minor cleanup. Nils Anders Danielsson **20080312134702] hash: 0000000542-c139032fe76bc30a16627d75017657c0b1fb9194c50d5e6d9abd6bd243cb379e [Imported some missing modules. Nils Anders Danielsson **20080312134808] hash: 0000000218-68181e31cbc7a86e3c64320dc16b592ead9a1a873d0eb9cbc9b3eb4257fe3c0a [Added comment. Nils Anders Danielsson **20080312210935] hash: 0000000307-ab3eba9ec2c074ac17804b130265fc9eaba2efabbdb12dfee5f7fbc0f8382574 [Updated code to reflect changes in library API. Nils Anders Danielsson **20080312210949] hash: 0000000330-c16b9b3030e8f6853158b2f5db099661d682833c7dd093419c8462e6850db916 [Renamed Model to the more correct ApplicativeStructure. Nils Anders Danielsson **20080313163645] hash: 0000002276-7b6dc969be7ebb7f5f471b56ef8c7b6141677789b25bf5e38afe02694c71ea24 [Updated code to reflect changes in library API. Nils Anders Danielsson **20080430223335] hash: 0000000391-303fc9ec452297d4d99a82d6c2235a799491870469fcf9f7efe0231ef2ac5378 [Fixed a comment. Nils Anders Danielsson **20080710184237] hash: 0000000456-ec6f944f0ee398896029aa29b5e8b330975c7c16204ba26a326a02c6da440de9 [Updated code to reflect changes in the library API. Nils Anders Danielsson **20080710184614] hash: 0000000487-cb703b120e69964a3c365f5b3ecb1d234eb4c712895f80c50fbaf4155ccf99c7 [Mirrored the development using PHOAS instead of de Bruijn indices. Nils Anders Danielsson **20080710185538] hash: 0000005382-b09643071c116bac49b50d9f481cd12dee0a9f89f0cab82ee9f6276d986c7370 [Added a condensed version of the HOAS.SimplyTyped modules. Nils Anders Danielsson **20080711142214] hash: 0000001998-5b5a5145f7694e757f8b49509e1b9a80b2d5c80bb5c404b3bfa1a19c05c023a3 [Updated the code to reflect changes in Agda and the library API. Nils Anders Danielsson **20090408103917 Ignore-this: d750703da1a696ccb11e6048cb232072 ] hash: 0000023783-e124bce36ac6f6c73df6b7d4e64dc694d016f17b6c43960a7717a96eae05b62a [Improved the documentation. Nils Anders Danielsson **20090926123201 Ignore-this: 6b1ea9c82a426886ada7a31c1c3d4237 ] hash: 0000000641-71ddb8acd983f2d98764ad365b16314b37cd1e9fbf662334529051ebffc6c345 [Updated code to reflect changes in library API. Nils Anders Danielsson **20090926123234 Ignore-this: d566c13a5c38fa677fb7b33f6401dc7a ] hash: 0000000437-ab51deb50a164fa9865a26cfddb07959cf94702ac0937cae935a2656f6367f41 [Clarified the status of the Semantics module. Nils Anders Danielsson **20090926124103 Ignore-this: 86e8379c7a40659af5044a5763ddd878 ] hash: 0000000245-fc50c751e2a661fd23b5b44ccf9e6a31b58090266638b7a2517812eee81255bb [Updated code to reflect changes to library API. Nils Anders Danielsson **20101026120229 Ignore-this: 47d2e7cd679f04565e818e3842ea17c2 ] hash: 0000000910-1e02efef629dd14b5782efe1d6585e2d5061d0e683c4c4f0155699323c4a37cd [Updated code to reflect changes to library API. Nils Anders Danielsson **20110516144820 Ignore-this: 167315136b5ef5f3689596ddf1e2f2a2 ] hash: 0000000317-680ad05aabf2552fd4cad5fa26cc45830dd64a26f82919440e2b62edc86783b4 [Added a .agda-lib file. Nils Anders Danielsson **20161208094702 Ignore-this: dba0c3c5e611dff7e09c929ab1ce6378 ] hash: 0000000272-6b81a5eecb7648a9f71ea80c97e99231d052e2a2e5e4cbff4ca63b934403c467 [Made the code build using recent versions of its dependencies. Nils Anders Danielsson **20161208095608 Ignore-this: f02c89d1d3981b5b8ee935248331454b Dependencies: Agda and the standard library. ] hash: 0000000877-41940b61e6c7840e7552f31291ba0747ef4975e9db8bd639ac5e1914405cf97d