Skip to content
Merged
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
0514e09
proof(coq): Phase 1 — cfg-remember + atomic-axiom tactic on Lemma B (…
claude May 24, 2026
7acf1e5
proof(coq): add subst_preserves_typing_strong (unlocks Cluster A of L…
claude May 24, 2026
96efe22
proof(coq): Qed output_ctx_det — output-context determinacy for has_type
claude May 24, 2026
d97ba32
proof(coq): Lemma B — close 3 Cluster A cases (S_Let_Val, S_LetLin_Va…
claude May 24, 2026
9a03df6
proof(coq): Lemma B — close all 7 Cluster A cases (S_If_True/False, S…
claude May 24, 2026
d4161b6
proof(coq): Lemma B — close 4 Cluster C cases (S_Fst, S_Snd, S_Copy, …
claude May 24, 2026
68712fc
proof(coq): Lemma B — close 10 Cluster B congruence cases (35->11, 69%)
claude May 24, 2026
a2e8bcf
proof(coq): close S_App_Step1, S_App_Step2 via sibling type_determina…
claude May 24, 2026
ad5f299
proof(coq): Lemma B — Cluster C complete (S_StringLen atomic, S_Regio…
claude May 24, 2026
cf058e3
proof(coq): introduce step_preserves_type sub-lemma (partial; ~15 of …
claude May 24, 2026
f499c82
proof(coq): step_preserves_type clone-out — 8 more cases (12 of 35 re…
claude May 24, 2026
eed4901
proof(coq): step_preserves_type — close 4 cases fully, structure rema…
claude May 24, 2026
50ce303
proof(coq): step_preserves_type — add step_R_change_shape, close MIDD…
claude May 24, 2026
caa424c
proof(coq): step_preserves_type — close 7 RIGHT sub-cases via members…
claude May 24, 2026
efbe083
Merge branch 'pr-125' into merge-pr-125
hyperpolymath May 24, 2026
f696497
Merge branch 'main' into merge-pr-125
hyperpolymath May 24, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view

These merge commits were added into this branch cleanly.

There are no new changes to show.