Skip to content

Commit d0e34d3

Browse files
hyperpolymathclaude
andcommitted
chore(submodules): advance wokelang pointer — value_eq_dec constructive proof
Picks up 66fe1a4: prove value_eq_dec as Theorem via decide equality + Req_EM_T (no Axiom — uses Coq.Reals' existing classical imports). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 0a92ee2 commit d0e34d3

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

wokelang

0 commit comments

Comments
 (0)