Intro pattern equivalent of `constructor` - Githubissues

verse-lab / lean-ssr

LeanSSR: an SSReflect-Like Tactic Language for Lean

Apache License 2.0

31 stars 0 forks source link

Intro pattern equivalent of `constructor` #12

Open dranov opened 7 months ago