Skip to content

make hypothesis name compatible with user choice#11

Merged
ZRTMRH merged 1 commit intoZRTMRH:mainfrom
JadAbouHawili:level4-hint
Apr 18, 2026
Merged

make hypothesis name compatible with user choice#11
ZRTMRH merged 1 commit intoZRTMRH:mainfrom
JadAbouHawili:level4-hint

Conversation

@JadAbouHawili
Copy link
Copy Markdown

Implement {h} as suggested by lean 4 game docs

@JadAbouHawili
Copy link
Copy Markdown
Author

@ZRTMRH ZRTMRH merged commit 2c0778a into ZRTMRH:main Apr 18, 2026
1 check passed
@ZRTMRH
Copy link
Copy Markdown
Owner

ZRTMRH commented Apr 18, 2026

Thank you! Merged.

@JadAbouHawili JadAbouHawili deleted the level4-hint branch April 18, 2026 19:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants