{"entities":{"Q7361000":{"pageid":31518539,"ns":120,"title":"Item:Q7361000","lastrevid":105362363,"modified":"2026-10-07T13:34:12Z","type":"item","id":"Q7361000","labels":{"en":{"language":"en","value":"With-Type \u2013 Poor man's dependent types"}},"descriptions":{"en":{"language":"en","value":"AFP entry With_Type"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1bb541b794c4e97cb4c4f85a0508a6d94a8a2dc4","datavalue":{"value":"https://isa-afp.org/entries/With_Type.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361000$8546A887-3A2D-461E-AFC8-41B78CD6350B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"23ae4fe473a8a206d8424d79281bf861ccf12a8c","datavalue":{"value":{"time":"+2024-08-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361000$2D0F5C91-9E83-4826-AFF8-FD51CD09A82B","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"0f726647cf47955102e00c4d9747edb7ccbe5fa2","datavalue":{"value":"Dominique Unruh","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361000$9C7644E7-C37D-4E6A-95CE-35CFE2C106D3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"100d856f8cbc5ffd8446fca55efade1405410ffc","datavalue":{"value":{"text":"With-Type \u2013 Poor man's dependent types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361000$BD7959BA-012B-4E6E-BDD2-51307448F4C3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4cb88c6aacad14a187f194127dae25bc38a79da1","datavalue":{"value":"The type system of Isabelle/HOL does not support dependent types or arbitrary quantification over types. We introduce a system to mimic dependent types and existential quantification over types in limited circumstances at the top level of theorems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361000$B09EAA2A-EB93-4950-9C57-F4A09C54CE32","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a1a0dcbfc561e1e5ffac774e9501a5c3c966797","datavalue":{"value":{"entity-type":"item","numeric-id":1722645,"id":"Q1722645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361000$2829F7AE-2503-4198-9501-D7E907A78B80","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":"Q7361000$D38DC977-4D62-4BCE-B015-3B9A700B43A2","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"924412e4302451de51094e930f82bf07674a31aa","datavalue":{"value":{"entity-type":"item","numeric-id":7361105,"id":"Q7361105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361000$51FDB350-79A1-4B44-A51E-87E2F0BC3CDF","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361000$6AF85443-581D-41AF-81EE-F78CF1B7478F","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":"Q7361000$5CA7AE73-645F-4EC9-9623-E4DF9FC32EE5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"With-Type \u2013 Poor man's dependent types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/With-Type_%E2%80%93_Poor_man%27s_dependent_types"}}}}}