Skip to content

feat: Add first EvalT and ProdT Interaction Lemma - #1344

Merged
jstoobysmith merged 16 commits into
leanprover-community:masterfrom
NicolaBernini:feat/add-first-EvalT-ProdT-Interaction-Lemma-1July2026
Jul 4, 2026
Merged

feat: Add first EvalT and ProdT Interaction Lemma#1344
jstoobysmith merged 16 commits into
leanprover-community:masterfrom
NicolaBernini:feat/add-first-EvalT-ProdT-Interaction-Lemma-1July2026

Compose HEq casts in evalT product proof

0e6ef53
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
Python based style linter
succeeded Jul 4, 2026 in 13s