{"entities":{"Q40306":{"pageid":40362,"ns":120,"title":"Item:Q40306","lastrevid":105426980,"modified":"2026-10-09T10:06:34Z","type":"item","id":"Q40306","labels":{"en":{"language":"en","value":"Datatype Order Generator"}},"descriptions":{"en":{"language":"en","value":"AFP entry Datatype_Order_Generator"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"060d2a65f434a7c145e898e015e17b972df0a3b6","datavalue":{"value":"28592","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40306$35AA021E-DA0C-47AC-92AC-10B0D3CC7256","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":"Q40306$CBCFE406-B1FF-4B46-81C3-A0134D6AB373","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"7b531884501be5bd23f80dfa598d62c659682df9","datavalue":{"value":"https://www.isa-afp.org/entries/Datatype_Order_Generator.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40306$38DDF86B-1E43-4CCB-A0A8-E2880069D488","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40306$29AF83BB-21CA-4524-8058-BE56FCC271AF","rank":"normal"}],"P1458":[{"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":"Q40306$B436B415-7618-46B7-AA94-CD5A28097EE3","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":"Q40306$668B8D78-92D0-4BD2-8E81-78225D5D5B4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"acb83a4d262d787fb22b160cee44d797c18d249c","datavalue":{"value":{"entity-type":"item","numeric-id":1353374,"id":"Q1353374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$49DEE4BD-E2A2-4813-87A5-2815DC623F8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"083108faf337c7af517e32b440172fa2ec83c61c","datavalue":{"value":{"entity-type":"item","numeric-id":5973381,"id":"Q5973381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$8F092399-FFC2-4F9E-97BA-1D378D8BD929","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f5cf1c799fbe6d303f4d3cb6807bd68c09cb6169","datavalue":{"value":{"entity-type":"item","numeric-id":1353381,"id":"Q1353381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$24D8B6FE-7FE7-4127-AC3C-C080F5DA57C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c07dad7b9d1fb6cf6c1ef6118cf06bc6823ad96f","datavalue":{"value":{"entity-type":"item","numeric-id":1353377,"id":"Q1353377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$1D753CF7-3E77-4025-90B3-87B19BAD3FC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"feccd3116831194613b0ee92ed8475cd8805d11f","datavalue":{"value":{"entity-type":"item","numeric-id":1353379,"id":"Q1353379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$325AEF06-8F03-467F-AECA-AB134AA29DA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"243c22083d5dd4306f94079fe846ceb27f90489b","datavalue":{"value":{"entity-type":"item","numeric-id":43946,"id":"Q43946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$06170A2C-DFD0-4D60-8AC5-3F1042389620","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$2D627838-946C-41A6-81F2-64A5BF473EBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$4467AF87-616C-482D-9BE3-D07744D54826","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":"Q40306$1CB46EEB-4458-492C-98AB-9A460FCE95C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"896262f806b2b78fa79739c4fc9e5155ef235490","datavalue":{"value":{"entity-type":"item","numeric-id":40250,"id":"Q40250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$A98C78ED-EA77-48CF-9FD2-6872CAE21DD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6a1564a2a71a8bc8258028a3b3d3d16a3ca49720","datavalue":{"value":{"entity-type":"item","numeric-id":40952,"id":"Q40952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$4B8092D4-7A8D-4D03-AF96-78822AC0AFBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2380ac1a12e996d3fb11c13b134f7ff73eba1d5e","datavalue":{"value":{"entity-type":"item","numeric-id":40305,"id":"Q40305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$6E33B12D-017F-43BD-BAC0-BF6C6BA5E8BB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9e699362cd467b88f896a96e13e782fba4ae9ca2","datavalue":{"value":"https://isa-afp.org/entries/Datatype_Order_Generator.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40306$EFEB3E4F-289C-48E6-A68C-1BA2D044EEE1","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q40306$65A9166F-3E8F-405C-9AAE-B9CA855B0718","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"530d54f5a3a0e40191ce727f9487d3cf7ab860be","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 (linear) orders or hash-functions which are required in the Isabelle Collection Framework. Moreover, for the tactic of Huffman and Krauss to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework. Our formalization was performed as part of the IsaFoR/CeTA project. With our new tactic we could completely remove tedious proofs for linear orders of two datatypes. This development is aimed at datatypes generated by the \" old_datatype \" command.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40306$7848BC78-7CE5-4635-BF51-E4B6F4D4C2F0","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":"Q40306$E80ECEA1-D8CE-4739-AFF5-2A1A761F9254","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":"Q40306$E1ABDC60-2F6C-4F6A-B2BA-DD906826CA52","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":"Q40306$C4279B1E-9FF3-4677-A19D-E5DD60969EED","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"edaae9fe0e5779978f85e3c7bb7897012bfd4b62","datavalue":{"value":{"entity-type":"item","numeric-id":7361610,"id":"Q7361610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$3175A75C-A769-40FA-9E35-01730610B174","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"1518b44e9920a7e58377edf0d25bb1683f308560","datavalue":{"value":{"entity-type":"item","numeric-id":7361163,"id":"Q7361163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40306$8968C868-F881-4967-80F5-82E81796FE11","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0d67a3f37d3d3502279c0a1bc8c57fa4be754247","datavalue":{"value":{"time":"+2012-08-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40306$C0887580-FF7D-4232-8012-1454307EC421","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9a56fe5a61ed52d0b67f6c0e18410997a1f4daa0","datavalue":{"value":{"text":"Generating linear orders for datatypes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40306$990B65D4-915E-4F2C-A17B-AE89D38AF3A0","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":"Q40306$0FECCC43-B3E5-46DB-A2C1-DAE6C878585D","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":"Q40306$7B91CA4F-AB96-49F3-9A8D-D588CFDE5BCE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Datatype Order Generator","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Datatype_Order_Generator"}}}}}