{"entities":{"Q7361555":{"pageid":31520204,"ns":120,"title":"Item:Q7361555","lastrevid":105368699,"modified":"2026-10-07T13:37:36Z","type":"item","id":"Q7361555","labels":{"en":{"language":"en","value":"Lifting Definition Option"}},"descriptions":{"en":{"language":"en","value":"AFP entry Lifting_Definition_Option"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"449f0ef7aa1d4a4186dfb3516f8b5b5bb80ed0c1","datavalue":{"value":"https://isa-afp.org/entries/Lifting_Definition_Option.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361555$FBD1E95B-D9E7-44F3-A6AC-DDA30AFE3C36","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0bd9ab9676ef0df75a1a28ac03b07e1906746565","datavalue":{"value":{"time":"+2014-10-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361555$2F9CA998-AA6B-4745-89CC-49ADEF9A4252","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361555$0450F354-BC6B-4228-8858-DC29D9CB9DC5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"72672584c64be66c34342e6b2230c2f2ff8dabd6","datavalue":{"value":{"text":"Lifting Definition Option","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361555$20015794-3512-45D5-8B1D-D45A4CECE36D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fefdeea97b472d0e0c252d50cd47b829f3d87294","datavalue":{"value":"We implemented a command that can be used to easily generate elements of a restricted type {x :: 'a. P x} , provided the definition is of the form f ys = (if check ys then Some(generate ys :: 'a) else None) where ys is a list of variables y1 ... yn and check ys ==> P(generate ys) can be proved. In principle, such a definition is also directly possible using the lift_definition command. However, then this definition will not be suitable for code-generation. To this end, we automated a more complex construction of Joachim Breitner which is amenable for code-generation, and where the test check ys will only be performed once. In the automation, one auxiliary type is created, and Isabelle's lifting- and transfer-package is invoked several times.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361555$6C091008-A00B-4153-B3F7-BBCD21E96223","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"16b4b9eb7104682bb03b01e94a3a4f2c998deb92","datavalue":{"value":{"entity-type":"item","numeric-id":385988,"id":"Q385988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$C0AC9E1F-4BBF-4CE0-BFF1-3DF00DA03495","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$A98ED2AC-253C-4D97-ADCC-CE2D22105B30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c45ba14d12e09f456e25dae92d898457f6d44bd","datavalue":{"value":{"entity-type":"item","numeric-id":2380983,"id":"Q2380983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$790E390B-F947-4AF9-A88D-B40597A0C77F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"931c42c28f22f89fe1b66164f9ececc2021ac1a2","datavalue":{"value":{"entity-type":"item","numeric-id":3558332,"id":"Q3558332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$85929C21-2BE3-4800-9A47-445AD1B21872","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25b684db5c89aba28ac479c116014841dfb39a90","datavalue":{"value":{"entity-type":"item","numeric-id":5327333,"id":"Q5327333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$4BBA8FC1-BF63-41C4-B49C-5AE6A30A4410","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0d795517e293a55fbffeee6d84c637293c8bf8","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$A5159A98-E148-4F90-A50F-12E28A164D39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c704d43a48e07ac24cfe13985bec3bdd1a17595","datavalue":{"value":{"entity-type":"item","numeric-id":834373,"id":"Q834373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$3FA18667-6C4A-421E-A1CD-ECBF528DE862","rank":"normal"},{"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":"Q7361555$75E01B01-703C-4D0D-B460-49660AC10F65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f0278a622341c2c3ea684f66af68a5b07b0b894","datavalue":{"value":{"entity-type":"item","numeric-id":972425,"id":"Q972425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$EA53E373-06DA-4FEA-A368-1F7DCB73E829","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":"Q7361555$06997BC5-3E06-409E-881A-244782682D62","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"eff161b7dcf55a20ec4d840b7f18d4148cc115e3","datavalue":{"value":{"entity-type":"item","numeric-id":7360789,"id":"Q7360789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361555$E4116184-37C6-4930-86D2-71B95500EDFE","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":"Q7361555$A6FC94C5-A5DB-4961-8882-DFBE8211406E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Lifting Definition Option","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Lifting_Definition_Option"}}}}}