{"entities":{"Q7361764":{"pageid":31520831,"ns":120,"title":"Item:Q7361764","lastrevid":105368897,"modified":"2026-10-07T13:37:39Z","type":"item","id":"Q7361764","labels":{"en":{"language":"en","value":"Coinductive"}},"descriptions":{"en":{"language":"en","value":"AFP entry Coinductive"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"dec911e73d544cc024810ccabe487c76b1c9e248","datavalue":{"value":"https://isa-afp.org/entries/Coinductive.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361764$2FFD3A0C-500D-4A56-A73A-E8812CDCB117","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f701a5fb7efb18b2a5b2faa4325ff6ec6c98bb41","datavalue":{"value":{"time":"+2010-02-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361764$CE4DF39E-A2D6-4C17-A6EF-DBC30F43ADAF","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"480a99c095fd0e6e30ce40dd951da46a627a2bb9","datavalue":{"value":"Andreas Lochbihler","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361764$5F3B351A-D3BC-4938-84E8-316F7E3AE7BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"01b202f25e5390ba0104cc409e25272c5fbddba4","datavalue":{"value":"Johannes H\u00f6lzl","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361764$C364D542-FCA6-49D7-80C8-4D8AB245C5F9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7c14e209a0e7a4073395d9361946c30c8f7f0ad3","datavalue":{"value":{"text":"Coinductive","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361764$C4F32012-0539-42DA-B369-508E55B791E3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ebc7755f07e164c686dfcc63e378e35f287f3949","datavalue":{"value":"This article collects formalisations of general-purpose coinductive data types and sets. Currently, it contains coinductive natural numbers, coinductive lists, i.e. lazy lists or streams, infinite streams, coinductive terminated lists, coinductive resumptions, a library of operations on coinductive lists, and a version of K\u00f6nig's lemma as an application for coinductive lists. The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361764$EA52CA14-58ED-4DE0-AE94-AD3587389A89","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":"Q7361764$369E03EE-166F-4158-9D1E-29F020C7F78A","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":"Q7361764$557FFD0C-3026-4A06-A083-95B57086126B","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":"Q7361764$AC161063-DCCB-4FF1-A59E-ED57EE4177B5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Coinductive (AFP entry Coinductive)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Coinductive_(AFP_entry_Coinductive)"}}}}}