{"entities":{"Q40300":{"pageid":40356,"ns":120,"title":"Item:Q40300","lastrevid":105426995,"modified":"2026-10-09T10:06:36Z","type":"item","id":"Q40300","labels":{"en":{"language":"en","value":"Deriving class"}},"descriptions":{"en":{"language":"en","value":"AFP entry Deriving"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"347153c5492043ca52940791a3939e1a6a282cd8","datavalue":{"value":"28586","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40300$A1DEA6B9-C88B-4918-9792-2BB6697F5312","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$3FB1EA93-CFFF-4ED0-9CC4-EF7267851E5A","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"435c5aa6dd8b713df65d35947e52516fd46bff30","datavalue":{"value":"https://www.isa-afp.org/entries/Deriving.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40300$1CBB2BA3-4E96-4BE9-8918-00755A3D9E12","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40300$85C51480-B3C4-42BE-8297-B24BF9ECBC01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40300$2DCDF5D0-242E-46E4-9183-5E3FC53A3630","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40300$1FDA7AAF-072D-4949-80B7-7FBE7A57188B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40300$D08474D3-3035-4EC5-B8A4-1ED8B221C96D","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"08c88936307628333e4216a96cc9b5068be0fdd7","datavalue":{"value":{"entity-type":"item","numeric-id":40290,"id":"Q40290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$3CE107C8-B4D2-429A-8421-1738E9ADF707","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8bf2731143fd82a1f95f40f13b2fce56fbb7345a","datavalue":{"value":{"entity-type":"item","numeric-id":40299,"id":"Q40299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$7E71B1C0-C795-4BAE-B341-637E49117BEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6953b82ed35a5241d6fb5d47b5912e5553edbeaf","datavalue":{"value":{"entity-type":"item","numeric-id":40298,"id":"Q40298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$C75C6113-931B-40BB-BF83-EE8E41B2FB10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"86103b3556b4d28c3d563e083deb1d8901ceb985","datavalue":{"value":{"entity-type":"item","numeric-id":40252,"id":"Q40252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$DC1BC0FD-DE3E-4209-850C-763621DD8672","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2f0eb5498f624eca19e760cd08d6ae2738f933e4","datavalue":{"value":{"entity-type":"item","numeric-id":40251,"id":"Q40251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$B5BF5767-06E7-4DC5-BE42-0F159E8D8000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"937a19baf3283c91e89f0a08dd8e59bb640da883","datavalue":{"value":{"entity-type":"item","numeric-id":40624,"id":"Q40624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$42B1E3C3-AE19-4E46-A4F2-802A3FF86904","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$EF982EC8-C979-4871-84BF-258709487ED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$936AB9D2-07AD-4F6B-80FB-C760CF7124D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1cebaec1d4c924093d2802f1f6f7d4f984bb7f11","datavalue":{"value":{"entity-type":"item","numeric-id":19148,"id":"Q19148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$F7C76867-80F6-49EE-BC82-62DF160B5141","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"85d5a2bfb7e5cd7e1dfb166523d6500a685410a1","datavalue":{"value":{"entity-type":"item","numeric-id":13377,"id":"Q13377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$498E0E62-C32B-4AED-94EC-98BE03586FCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$A10234F0-174C-480F-9742-FA5F2CAAFB95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$38086409-8CCA-4246-B784-10411FED6CC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$60F41C45-42D8-4FA5-A199-60A4BE138669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a0a329d132b963c571723538ca5cd1b467b324fe","datavalue":{"value":{"entity-type":"item","numeric-id":40325,"id":"Q40325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$3C6E215B-A77D-4557-A5C5-4144B7FB406A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$2FF413A9-17C0-4A57-A305-A6537EF972BA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"60e2f546955810db82e49259edde2e096c770cc3","datavalue":{"value":"https://isa-afp.org/entries/Deriving.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40300$04164B32-3610-4268-9D71-47BBD73275C9","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7335db8cbac804a8435e80e80636b4dde04d73bd","datavalue":{"value":"Christian Sternagel","type":"string"},"datatype":"string"},"type":"statement","id":"Q40300$2E205681-1A64-4966-8BED-EFAF0042DBC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q40300$3E6A1B12-864E-4CF3-9851-D0A5A90BBD06","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8611b7e2477bcca113fb0ded1faf83f282283902","datavalue":{"value":"We provide a framework for registering automatic methods to derive class instances of datatypes, as it is possible using Haskell's \u201c deriving Ord, Show, ... \u201d feature. We further implemented such automatic methods to derive comparators, linear orders, parametrizable equality functions, and hash-functions which are required in the Isabelle Collection Framework and the Container Framework. Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework. All of the generators are based on the infrastructure that is provided by the BNF-based datatype package. Our formalization was performed as part of the IsaFoR/CeTA project. With our new tactics we could remove several tedious proofs for (conditional) linear orders, and conditional equality operators within IsaFoR and the Container Framework.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40300$A198F571-5384-46D3-A60E-9BF4AFD10573","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0aef60bd392ccfb5e82daa98f095917b33d1745","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$9B3C4953-6B3C-4184-90E6-BBD7C456B9B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7a1ce015f9a6115f5e15ce96a4b6a73ac4d89f9","datavalue":{"value":{"entity-type":"item","numeric-id":5327340,"id":"Q5327340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$338BD251-9A14-425B-B2BC-8093D79B4D08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a5a326924c9f9f3cf0f5061fb0ff950ccfad0d","datavalue":{"value":{"entity-type":"item","numeric-id":5747660,"id":"Q5747660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$DAD3025B-D291-461D-B4FE-204BC35491AF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"aaa340ae51925f6905d18399dfd97774b2ad90cc","datavalue":{"value":{"time":"+2015-03-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40300$F3D22F2D-F3E9-45E3-BD8B-C0CD61507AC0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5bd5a2f8eb11ba81af6410e9364a632bd641e383","datavalue":{"value":{"text":"Deriving class instances for datatypes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40300$4AD6AE8D-3934-4F8F-8B5C-65B2AF3154F2","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$8763F444-AA46-4F5E-B606-F98B3E054BBC","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"f0d6ccc9a00d2d1e3be7ec2239689671c14dec25","datavalue":{"value":{"entity-type":"item","numeric-id":7361918,"id":"Q7361918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$C22A34BE-278A-4447-92B8-DB93C0FE4362","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ef7bddd24a035fe32f48fd95ea6033928a9b8e67","datavalue":{"value":{"entity-type":"item","numeric-id":7360788,"id":"Q7360788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40300$CF1891A3-6BCD-4E26-8A1A-87C8A8DBD629","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Deriving class","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Deriving_class"}}}}}