Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

choose … using still triggers a warning #63

Closed
TentativeConvert opened this issue Nov 25, 2024 · 2 comments
Closed

choose … using still triggers a warning #63

TentativeConvert opened this issue Nov 25, 2024 · 2 comments

Comments

@TentativeConvert
Copy link
Collaborator

For example:

Robo/Game/Levels/Quantus/L11_DrinkersParadox.lean

Line 65 in e294c8a

choose p hp using h

In the game, this still triggers the warning

The tactic using is not available in this game!

(both on adam and on adam-dev).
@elimohl
Copy link

elimohl commented Jan 14, 2025

Same for Surjektivität 6.

@TentativeConvert
Copy link
Collaborator Author

Should now be fixed on dev by:

Robo/Game/Levels/Quantus/L08_Exists.lean

Line 90 in 4c35653

NewHiddenTactic «using»

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@elimohl @TentativeConvert