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

Add other tactics with as #1

Merged

thomas-lamiaux merged 2 commits into thomas-lamiaux:intro-patterns from Villetaneuse:intro-patterns

Jan 3, 2025

Villetaneuse commented Dec 30, 2024

also correct some whitespace issues and add a small remark after the first "destruct as".


          Add other tactics with as

65bc16d

also correct some whitespace issues and add a small remark after the
first "destruct as".

thomas-lamiaux reviewed

View reviewed changes

src/Tutorial_intro_patterns.v Outdated Show resolved Hide resolved


          Update src/Tutorial_intro_patterns.v

d777063

thomas-lamiaux merged commit e692a9d into thomas-lamiaux:intro-patterns

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet