e3e4205d52fb4a618630414a24d0d2f195c10e531a84228d2d07c0bead12c798  CHANGELOG.md
84b3c27748307451d04f3f3b3a7454020a24cb8bbf375625a9c787e88fdda1c7  CITATION.cff
06493476a22e73ee861eefb0e2bf9705a14ed1cc1b5900935e57827a8a020dc2  CODE_OF_CONDUCT.md
c445af13b7af18a8e2b50f9ec89562bc1c70439cf25a038bdace52c165c851ad  CONTRIBUTING.md
6a493a0f4a776f6be4454eb951b271403a8c1226840f10ce7145c233a2c55078  LICENSE
6a493a0f4a776f6be4454eb951b271403a8c1226840f10ce7145c233a2c55078  LICENSES/MIT.txt
879d4cba189d906ac73c3194d2e1635fd148235fe4eb66d192974524170c7fa0  NOTATION.md
25bdb5074f3567ad9d1cab37bcf12084f2af9796cef8ff23f3f34c9229f560cd  README.md
107b0ed2be00b67fd3dc170f8f667695b2ee25fcb6f1c04704286d2728a467e9  REUSE.toml
8f26c944cab312c4cd063a7d1bf5781b18c8de2f7b0ad095e7b375f4082329a0  SECURITY.md
1e64287f91a9b6dd890382cc22c928abb55fb00313d4815b955b25c47daf2dc1  THIRD_PARTY.md
1f930dd1f133c1f97a94fe3acb8db34372cf4c01ffdb2b3ff4ca72f9494121e9  VERSION
b6e240ada08b173aa80123536b72097578d0e7b0b54f95ef4fa901a980f09d1a  agda/CertRender/Cert.agda
df67f45d24b5341ea26c814ccd23fc2968d39897cbcd8f031ee44539ae3aeec6  agda/CertRender/Fixtures/P10/FxOrder.agda
6c2add3e396816394c852945196119f5d506baff638d2ff59744705f94315e5c  agda/CertRender/Lean.agda
fb2919348bae32a5e9745534dcded34043238cb0c10b8acab83d7b17989df0d2  agda/CertRender/LeanSrc.agda
b95907b1e2f16cb5c656f59041172e363bd27aae9f197f21360818adb27b4a4f  agda/CertRender/LeanSrcRoundTrip.agda
736b3ccb9f83901ff445976cf3ebe45a84b3aa8e24529acd629ec8af1d20bcbb  agda/CertRender/Main.agda
466151b75d8f82631036bf82b2923115f0ba029ea74e591b005ede92fc793966  agda/CertRender/MathML/Faithful.agda
2eba075d56225c065e58cb9915499f61f99b7f2bd5bb999d67db2cc91dc16b9c  agda/CertRender/MathML/Tree.agda
38dab3cf2ee431ad763bb7020f8f66e8c2c3d6ceafc0f38fff10183769fb34db  agda/CertRender/MathML/XMLText.agda
83a42cbecb33b9686d1363d1561d559f36ca67d38db03f2066dd940b238a6bd4  agda/CertRender/NatDiv.agda
657aa5f1230c34deef8a0a1b939fd438d2810a754f03aa25ca3fa59a617658cd  agda/CertRender/SIR/Serial.agda
e5646c3a1dfaae990a96db6ae613cc4b0d17588fc9a0a02fb98be97db3252195  agda/CertRender/SIR.agda
17e522cbb590a9bded0e4f0149acadc867985165b9a6d6d027d1e39f265c176f  agda/CertRender/Src.agda
42cd6a62f921a300f8d0d7e8ab036ab148c7d7dba92e888b7f7552a4e683ff8d  agda/CertRender/SrcRoundTrip.agda
4df4739e857b7abfb0f9fe3be93ae45810e9919d4f7530ac9b11bf9009cf3f70  agda/CertRender/Table.agda
d1259da551ccb6556e34122547c2cd684957d57186b343ca046e37a7bf4fe255  agda/CertRender/TableWF.agda
5ca58688d9c7ba80783b964393b2ffb2a6febf952f6b837c0013419a21296752  agda/CertRender/Tables.agda
1ff485bd187679e977a6f9e3948e4086a829407ec70d7a2cade3224cff8e82c7  agda/CertRender/Tests/MathMLRealizer.agda
9bd78fe5c78aee0567aeb9f6d1446abe9db90055f3de30b22a7a05854bccfa0a  agda/CertRender/Tests/SerialRealizer.agda
9c2c7e1b25c2bae62e66293f4193f6823ead182a128e189c78699624c384cfb4  agda/CertRender/Tests/SrcRealizer.agda
4d60b9bd7484fc6a517437a40b4ab912ea1759591ca708d5044354e9f6452050  agda/CertRender/Tests/TablesBad.agda
c4f834f2cc12786acef71f92e81240311b8a079458384e8aa2f2f67d3bd6620a  agda/CertRender/Tests/TablesWF.agda
41180bd680b2352fad7687e6735752d594c6a7e8c245130b1d04c1c43cb91db0  agda/CertRender/Tests/TexRealizer.agda
7a16a381f2c2b91345627059390c4c3a2aabff1f40f22ebe6c074ac0d87c22ea  agda/CertRender/Tests/TextRealizer.agda
1884ae93a82d21496f39d8334690ba880d1f22b82049098971aa0a771b8afc70  agda/CertRender/Tex/Faithful.agda
c91e4bf605e78a2fa3de53d5c845ed7ee033111c8aadcfa647ccbc11ca5b9924  agda/CertRender/Tex/MarksLemma.agda
d77e2be9a8645146d9bf0e77322254f91f2e7f667528d2c380f0e41a6debb1ff  agda/CertRender/Tex/ParseMono.agda
1ed4b936fe7421b13d9e857c65dd6b23c819949f088c7cb8df5581e9121a86ae  agda/CertRender/Tex/RoundTrip.agda
542bb5e0cbffaa7d5679578134c527c24877b37f502d49dafce9a43c23ec2443  agda/CertRender/Tex/Support.agda
02b2f5a22fbff429b2d2d1a4556404c77a8ca6840eb0c2f836463e617875c09d  agda/CertRender/Tex/Supported.agda
ddea688fd84e0638fe965e77790ba048903bec6932a4ee62f2919d57a67f169c  agda/CertRender/Tex/Text.agda
519696b4fad09fc7570a3c336371aa20903474d3ee7e667787ef408e5ce105ee  agda/CertRender/Tex/Tok.agda
fe0ab7fce676ee5425133d6eb8a67319209e5343bff82f812f125d93ef94ceec  fixtures/FxCohesion.agda
84b066c24ce2c0572755eec494d31f7e39be48880fa1c99e6ad315cbafd879ef  fixtures/FxCohesionHidden.agda
3b2461b2ac700b0356b6862abf72dc8989ff9c0fdf6ae126ea300e5c027abd01  fixtures/FxErasure.agda
0225aa4e35b2e3cb426040f194c4463c330cef58cc4a0bbe2dbf239e764353c1  fixtures/FxGuarded.agda
1d4d072ca203053dbf9d4602f3cc5ec59a37e45cd3827bf8e861bf79bdd653a8  fixtures/FxInstance.agda
cea56e6c84f5786c2381501cb1a8de210a02e8b79a54d16acfe834bf08dd9453  fixtures/FxInterval.agda
c09c97dedbe1f75f8f053918236f5985483b5ac01ed6809c445702aa43dce858  fixtures/FxIrrelevant.agda
a3117b242dedef504c502811a7da9661120ea019c61c0609dbe5b36a92c45138  fixtures/FxLevelUniverse.agda
24786b6cc47b416e848f185b7c14596f83cdab6e888f9f0fe4fc1c906b737951  fixtures/FxPolarity.agda
0e47ff2041da03a1ac1a4875818ef43ba8c596ca805ca4a2c8f377853ace5dee  fixtures/FxPolarityHidden.agda
3daaa04797399ba5ed3f8f5f5b1f40afac7f3f9e68b5602231bfadc1a6ad6397  fixtures/FxProp.agda
dcdaacb6c98282fcef62a883a114d4bb85ae040d81e531f608f810ec753ab364  fixtures/FxQuantityOne.agda
58647bf13a5733e9d790eb2d163eb672b5c60009efac180fa4c1f3591b8031b8  fixtures/FxSetOmega.agda
0ec92d83c6b085329e339a756f6060da6c75bd7e1d4b4e21d4d3f57ef1d21928  fixtures/FxShapeIrr.agda
0bb6f84c3a50063d1bebe98846c4d3a53fa5e188d4872e5c5da98d7021582aa5  fixtures/FxSized.agda
5e6067ff1996827ae737c0d04702edacb10f100c58d1c7dbbdaa0b9c889958cb  fixtures/FxTwoLevel.agda
84e511e231c5349bad71bd92083a52b72d093ddb38eb5493eac74d5c9a582d51  install.sh
eeb78a3931ef8526402971f42cc548270efeb3e324f6f349a1e56910cf16b430  release_check.py
5a33ad582118696d63bd9ea512dd076a7b01d53f299f2f8c9d08788726b73e0f  run_tests.sh
32d2bb317e7f9afe3c1b3935e32a4c82e074f93dd31eb2f314507191d7538ab5  scripts/check_cert_render_imports.py
ff4edfbbb219fe4a3c7a2d6c19e904e03592d4ddf44903a94b98739f1f8ad543  tests/expected_outcomes.json
f4a052055b61887522b3dcd9bb357d752fefddfc1063caf0fe4b35fa9ebe31b3  tests/fixtures_corpus.json
2ecf0f5f254ef171072c80275e33eceead27f92a89b1dbf5e2bca5646b4b6091  tests/oracles/p2_tex_oracle.py
73ee352de3b53a1eec6285ada0cab11e489b967f7b0a0f007f0818076c3aa5b1  tests/oracles/p7_check.py
e88d01b36e9fab72c3ca47e86df1c155925ac7a7b90b0db7cca3c93c40d7dca0  tests/p10_fixtures.json
316259e112beb8f8473fc615181c34101b0f0ef10b8155e8cd8482dd9cfc9a24  tools/agda_cert_render/agda_cert.py
02cb738b6e3b20781c5d02641d90e850fe9a6ec03fc08719ecbd9e1376b251c0  tools/agda_cert_render/audit_p17/DISPOSITION.json
419f4898667e4567de7b4ba0e5f1b82f0d4f589f0732d9f6537fdbdb625b316d  tools/agda_cert_render/audit_p17/core_check.py
574def20e9ead77a2f680828506853c5d199c5dd68c0cd80ee974a7a865a7a24  tools/agda_cert_render/audit_p17/disposition.py
efe9c241d2411b5da76c04063caca51e870fdcc8cd2373070c88b06bf908a5e8  tools/agda_cert_render/audit_p17/regress.py
c5478488c7aa8d63c0525b89ef49bbb2ea76bd70eed236b24edc9d8cb52ae678  tools/agda_cert_render/audit_p17/regress_kernel.py
8bb040b014942ea59c244bf9625d45a48d6f9b6f6202b77b300152642584c642  tools/agda_cert_render/audit_p17/regress_lean.py
b403bf62132cf5785a46ef2d62c63d67bb26c8f3e117fb69190a27526085e64b  tools/agda_cert_render/audit_p17/strict_cmml.py
db0bfab57f3418cf43db8ec12f066c3f26b1fba722250205ac9a88996a5cb759  tools/agda_cert_render/browser.py
b95433a94320fa1185f87a2818ea270102ca333ff786b81ec1497536b3ec0337  tools/agda_cert_render/cert_html.py
6e0df062090c68363ca35d20e33420ec54630f57c64d6406eaafd6ba0d81d6dc  tools/agda_cert_render/cert_latex.py
98ea361cbd478c804dace781d69a4ce0299c068d59b9a0ddcb3fa88db57a2b99  tools/agda_cert_render/cert_table.py
a3a0bdac9505bd4ce1eee4fa259478783bc4f99d94707e9688bf41f603da1a6e  tools/agda_cert_render/certify.py
4af442bc29ecc59901edda390cbae90430754bde344699b813580a4181e9f48d  tools/agda_cert_render/chain.py
c5bac118bfebe8d541b6f7fd58b82a5e51441c945e06087e079203b522ae8e56  tools/agda_cert_render/dedukti.py
1e88d40700886d60d4027b87be1f49b4e0dd883aa51a0c3880d95d7f61f38641  tools/agda_cert_render/extract/agda-cert-extract.cabal
4633e081ea3ef60dd56477c293d9945824ad2911efe7a71eac2caf2a7e5e0bdf  tools/agda_cert_render/extract/app/Main.hs
47d7af5cbd49b768a53905fa1dbf3ef5e57f35e9ca6b26d11f176cf2ffa3dfeb  tools/agda_cert_render/extract/cabal.project
894f5550db813568ff5de55ba244f3f317144c54ce4c11aaa189d4f672563e58  tools/agda_cert_render/extract/src/Emit.hs
54b1ef774347c4256f2835e5150f1860f7354812e4ead0de3f86b55f887ae2e9  tools/agda_cert_render/extract/src/Extract.hs
3c0307e52957756f28132511623441430a7c2f78c569c3efa213b638919c4f3a  tools/agda_cert_render/extract/src/SExp.hs
baeab1a316c8f2e66347531ca5a1908e996b94300f46846ae9bdf159e9b5ec1e  tools/agda_cert_render/extract_corpus.py
647cae45c3c9a734adaef9bc760b44bbbe7e3612925c5867d4ace00b8db1462f  tools/agda_cert_render/gen_tables.py
218324cf2a6332183d942b287f338ac57c890a145a57c3f6bf66a47da04fde14  tools/agda_cert_render/latex/agda-cert.sty
9fd5fad9b3c2c5abd370056e68827fdbe6e185865b347ba9d2bf0c962426553d  tools/agda_cert_render/lean_export.py
a886197ef736e50299a3d293dea5df4a96158d94297714a810ef358f776737f0  tools/agda_cert_render/lean_front/AgdaCertLean.lean
2a675f30f08fd295dc3a4b74d721b760e5580d95ce5ab60aef84c60984774ccc  tools/agda_cert_render/lean_front/fixtures/LeanCoreFx.lean
f40ad48e6350770e49fd2b8479ee5730b4896fed405aa2029fd376153e865268  tools/agda_cert_render/lean_front/fixtures/LeanFx.lean
dac2a3d636983cad2a8bb5b54d578d5bff62e406d40e16c6b9b2f9deb4df39c8  tools/agda_cert_render/lean_front.py
e16444a1ebd1e973ea4ee4bd1888648ec927bbfa07742c14b59cbc47f65990a5  tools/agda_cert_render/lit.py
77e5866723ffee0975fcd5f83588760e95318217cd51e7f63eff62dc45f1597a  tools/agda_cert_render/literate/LiterateDemo.lagda
912d650201bbb8c8c03ebe0ac7cc435513d9f722f24fe6ef94ebf9d92384d842  tools/agda_cert_render/make_corpus.py
da83269a0cb623cac03db4ff5c3c4fea8b958f9d649c1c7bd0301a14fa97d397  tools/agda_cert_render/mcp/README.md
3d611c6351a38335a25dc9cc99dd55597bb1336fd5a9001c2320bfd61832aa57  tools/agda_cert_render/mcp/args_check.py
43555d56ab129165cacb71f96e3dc6cc8e1dbd47c8edf2433ac220c8434be9e0  tools/agda_cert_render/mcp/capture_examples.py
decd5b344e792d56e840c8619c014c3cd4c27a46dfa7de78ed91b6034710423f  tools/agda_cert_render/mcp/examples.json
3c3284d202c3b08c2e498c4a170ee63842e2b199d739c87cd040f2fbc8a23531  tools/agda_cert_render/mcp/gen_registry.py
0cdee7562425cf9c442c830afefbaf43c78dc6ac70c5d376b0d5f6c96db6528b  tools/agda_cert_render/mcp/op_battery.py
5ddcc4f020fef94de1d495ca11dd36bf9a896b176908af84389d8edcacfba4c7  tools/agda_cert_render/mcp/op_certify.py
22ba168c799118e0329fc57b9fff39f0edde8679abf3899c2649327a44dd46d4  tools/agda_cert_render/mcp/op_chain.py
1356b19fc3d27cf516f0914b8a662939d3701c99a1da6b4e7008244ce9706cdd  tools/agda_cert_render/mcp/op_corpus.py
cc8e394860d669ae8f32e3ff91773dfeeee3898e558b726bf0afcfd709a4d720  tools/agda_cert_render/mcp/op_doctor.py
3c7eb469892170347a441f4425cdc0d074da9d4b82d9a04f443a73edcd4c8c51  tools/agda_cert_render/mcp/op_extract.py
9282b5b29c9b446aba98e4ccf7f747c8ea8e8871dc7565e8ac76ae8f037c32a1  tools/agda_cert_render/mcp/op_lean_export.py
c259fa0872769f20c3e56ae61a91b8421cff1ff4b0a51281729cccfb501fdc0f  tools/agda_cert_render/mcp/op_lean_statement.py
68d5efd1dc7dae9430a37a9389fca332be73a75187a8b6775bbb390192cc3a21  tools/agda_cert_render/mcp/op_receipt.py
66dfb84fa4c930c549697a7a6583523b2ac66e3394ef05f648e7d05ae6099490  tools/agda_cert_render/mcp/op_render.py
3dcd42f70352bc9ef0bbe90adee18cc963d5d4417335afe4557c603e568d312d  tools/agda_cert_render/mcp/op_verify.py
9dc6e3b73046855156565035a359e3dae2fe56a72847a73fed7db58e52015516  tools/agda_cert_render/mcp/ops.py
79d0d0d8f0b3affdee65c120da6e1f3cacfe82cc6bef17ed5e75cbe163d9345e  tools/agda_cert_render/mcp/patch_meta_skill.py
f8f90078c90eb77907cf5e03d80a9e2b111bc743cb883c2d1b4be226836088d3  tools/agda_cert_render/mcp/patch_query_tools.py
dce5fef2da604fc8b2a789604f3dee41b16cd9c1b3be071aa611802f20ef09dd  tools/agda_cert_render/mcp/retrieval_check.py
04ebbc7e8f766040612067441a5090b1bba1abb1019da3c09da1f132bb035ad9  tools/agda_cert_render/mutate.py
9d6b7f421ab19c7a8d5d4a341de9c1e9266fcd622e3a130e0f9e5c79b06965af  tools/agda_cert_render/outcome.py
08f31a41775fb2e9e4cda205706b12ae186651b5a353dd490bd02eb24d30cc03  tools/agda_cert_render/p14_audit/forge.py
03ee3a12ffc056c624c91bda798149b32746911fb8e763db0eaa681ac11b98bb  tools/agda_cert_render/p4_plants.py
116e428ecb2e4066e5b4a9382592e204a7697fd91229a6e07685c64d97ae1fa2  tools/agda_cert_render/paths.py
c1130566b8131ca6b4805e689d7310c369ffe14183f3248d68efb324ac262c06  tools/agda_cert_render/protocol.py
38448c6f3e1399308c8e73199029226c02c5e4931b2bfb03c90206cbbb213931  tools/agda_cert_render/schema/iaom_sir_cmml_1.rng
00c2cc2cfe4f793372a2ff5cce98dc6c575b4f1bfef1fe8391d0aba9ad992602  tools/agda_cert_render/schema/mathml3_strict_content.rng
cf7b0ff35865c27828836711c3ae66b17d3a24b96ccdf48bbc5f3eb997063405  tools/agda_cert_render/sirpy.py
e3eac345a41fe6add04f35a5684410e7eee6b0aab203e23c0ed78d372661726c  tools/agda_cert_render/tables/battery_map.json
c53f0a157ba9117a0e2ac154f06ab0a5c5d153db72d9e46647c8755394c849a7  tools/agda_cert_render/tables/category.json
2abd1072ce2da155d3cbb7234915167724148c9639afeabf9bd6d4d5587421c2  tools/agda_cert_render/tables/cubical.json
b9b740d98fe3cf2a3204a98052a121b88e1bffa175660a0cabef528d00424eb4  tools/agda_cert_render/tables/lean_core.json
72657f5534c3d425724b89de780e05c29147cd1d92bf70235d2e3ff7aa4fdf8b  tools/agda_cert_render/tables/stdlib.json
8a6da9887f6f2ad07afb27bde656ecacc58367a50c191ec851b0411f22870187  tools/agda_cert_render/upstream_repro/Collide1Shirr.agda
5390ae77951b8042aec355880a4892ec6b6ea65f49f2e9c96746988c84bee8bc  tools/agda_cert_render/upstream_repro/Collide2Qone.agda
c22dd6a19871890bed5e058022f03a864e281956aad8152062b93ecfd4cbbebf  tools/agda_cert_render/upstream_repro/Collide3Flat.agda
e40fe88bb5ec7d59837c52d331106133625d8fd2d339e93e4c43c03c62485e9a  tools/agda_cert_render/upstream_repro/Collide3Pol.agda
66b2dbb86c3f6ef02f22ff449bd5fe286ac307aefb721930e876e0aab114d055  tools/agda_cert_render/upstream_repro/Collide4SSet.agda
d4f46e593d35db117e3ea2568931533f1d78fba3c70a6d442cdd72423d1538d6  tools/agda_cert_render/upstream_repro/Distinct1Shirr.agda
81e3c039cfb7603e0d2fbd1794085f841935ed4238deac1411673d6c34e12af2  tools/agda_cert_render/upstream_repro/Distinct2Qone.agda
b3e37ab75b911ad9423d3bcef06d0057d6bdb3b148bd70f00cbc05ceb5172073  tools/agda_cert_render/upstream_repro/Distinct3Flat.agda
822654800acc1f423e9fcfba0c3767683c4f4766cdf8d61bec4f477919f448ea  tools/agda_cert_render/upstream_repro/Distinct4SSet.agda
e5e921807c1f4eea1e42ccb1fe3635818b33fd3a64a4dd959490294aafbefdfc  tools/agda_cert_render/upstream_repro/MEASURED.txt
2c015dc8e590471c36c8a94888e70bd03dba32a2cdd6cad5c7b759ad7568df9e  tools/agda_cert_render/upstream_repro/SameReflected.agda
8ddd49518f28d4e2eca994a31d7cc026484da4744b7dab7bf41b5c8e7f2d4a87  tools/agda_cert_render/upstream_repro/run.sh
