{"entities":{"Q6572535":{"pageid":14183690,"ns":120,"title":"Item:Q6572535","lastrevid":95765222,"modified":"2026-06-05T09:43:46Z","type":"item","id":"Q6572535","labels":{"en":{"language":"en","value":"Use and abuse of instance parameters in the Lean mathematical library"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7881117"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572535$DC64CA9E-C9A0-41A5-9DF1-3A4AB68746B8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2830f7557e72aeb27f1b80bd72e70a458a841df4","datavalue":{"value":{"text":"Use and abuse of instance parameters in the Lean mathematical library","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6572535$F9E803C5-F1FB-411C-B064-8A7297F8F8D5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc821230a7dc1550b9f8f0d5c6e779210c396b9d","datavalue":{"value":{"entity-type":"item","numeric-id":2102927,"id":"Q2102927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572535$0A0575CC-C706-4DE5-BA68-926815A5641C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7dae1a09e0b079923de71e99f58f11ff9161f5ec","datavalue":{"value":{"time":"+2024-07-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6572535$2E96388C-DE17-4F1C-90D5-EE39BF67CCBB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572535$B4BF2223-1E82-4CA4-94B8-20D238F7D25B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1f6580bb9bb517d59d64bbbb579ac49e576aa6d5","datavalue":{"value":"7881117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572535$0E839551-44A4-4149-8CCE-FAA65F4C7396","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572535$D687439E-C601-4BAC-8C4A-426E88D7431A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572535$A8248185-6AFF-4CC3-8DE8-D8F97196882D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0912ca4b29be2e77907d20f34cbe52ae2ffa70c5","datavalue":{"value":"typeclasses","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572535$0FFDF359-B0F3-4AFF-AEDC-00723EA910C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e8680952b101740d2661a75b00e2003d484a3f5f","datavalue":{"value":"algebraic hierarchy","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572535$D99EFA40-DC74-4C1C-B3FF-CA7E57D33EC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5de0940f2720db77a73ec7580f8f3ba4e460f459","datavalue":{"value":"Lean prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572535$07E69790-930D-4EED-A54D-E11F1B425538","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572535$802E1BB9-A5BC-49E9-B95E-2F00401CCCDC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"35b7c5f5e5b612d98ff5fb3d0f8bcfc77e08e624","datavalue":{"value":"10.4230/LIPICS.ITP.2022.4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572535$B091944C-6F12-4293-B431-905CEE090F8A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1dcc797c1c613dabe3eacc83d92ec424c9cfe4d","datavalue":{"value":{"entity-type":"item","numeric-id":2219408,"id":"Q2219408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e6e2e43aae996d570682f6a08183aaafaa55b61","datavalue":{"value":{"amount":"+0.7160388827323914","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6572535$298D15F3-875F-4BE4-AB5B-B03B1CF94B6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a60335246e1acbc61790885239378263dada0ab","datavalue":{"value":{"entity-type":"item","numeric-id":6118834,"id":"Q6118834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e2f838e2dee37ca020fe5cfade834e5236b740ac","datavalue":{"value":{"amount":"+0.6964197754859924","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6572535$4AF610D4-C565-4ED8-8FEE-668E44A7DC42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00741d8653e7ff3ed03255de9dc4a5ba9833efb9","datavalue":{"value":{"entity-type":"item","numeric-id":3094177,"id":"Q3094177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1971d92e85ceec701de7d812edbffc8e1a395a7f","datavalue":{"value":{"amount":"+0.6827618479728699","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6572535$5B7EE04E-E29E-42D2-AACE-563372C504F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2a0f2d2e0d757354645b6deff66dc677843b0a1","datavalue":{"value":{"entity-type":"item","numeric-id":2767927,"id":"Q2767927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5b3e26cc99ade1a6e483127ad08f35d27cab2dd","datavalue":{"value":{"amount":"+0.661415159702301","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q6572535$E8521CA6-47B8-4022-8103-579726277F7D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Use and abuse of instance parameters in the Lean mathematical library","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Use_and_abuse_of_instance_parameters_in_the_Lean_mathematical_library"}}}}}