Do not force type constructors to be injective#4259

Open

nikswamy wants to merge 29 commits into

Commits on May 14, 2026

Commits on May 15, 2026

Fix CI failures in Core type abbreviation comparison (#4239)

nikswamy
and
Copilot
committed

Commits on May 20, 2026

Merge remote-tracking branch 'origin/master' into _core_vs_rel
nikswamy
committed

Commits on May 21, 2026

avoid some needless retries if the guards are not allowed by the context
nikswamy
committed
remind myself and agents of clean-2
nikswamy
committed
handle terms marked with the injective attribute
nikswamy
committed
CoreVsRel tests: Group 17 mimics ha_val_core / Pulse slprop pattern

nikswamy
and
Copilot
committed
CoreVsRel tests: use try_teq smt_ok=true for fair comparison

nikswamy
and
Copilot
committed
Pulse prover: prefer no-unfold slprop equivalence checking

nikswamy
and
Copilot
committed
Core: add check_term_equality_head_injective; Pulse prover uses it for slprops

nikswamy
and
Copilot
committed
Tests: add Group 18 head-injective API tests to CoreVsRel suite

nikswamy
and
Copilot
committed
Core: remove step 2 fallback; mark forall connectives injective

nikswamy
and
Copilot
committed

Commits on May 22, 2026

Core: blanket slprop injectivity via unifier_hint_injective_type

nikswamy
and
Copilot
committed

Commits on May 23, 2026

Commits on May 24, 2026

Merge remote-tracking branch 'origin/master' into _core_vs_rel
nikswamy
committed

Commits on May 29, 2026

Core: equatable return type approach for slprop functions

nikswamy
and
Copilot
committed

Commits on Jun 2, 2026

Commits on Jun 3, 2026