Skip to content

Commit

Permalink
Merge pull request #303 from gihanmarasingha/patch-1
Browse files Browse the repository at this point in the history
fix typo in calc snippet
  • Loading branch information
Julian authored Sep 14, 2023
2 parents 417b7cf + 91dd270 commit ad8305e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion snippets/lean.json
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
"prefix": "calc",
"body": [
"calc ${1:start} = ${2:first} := by ${3:sorry}",
" _ = ${4:second} : by ${5:sorry}"
" _ = ${4:second} := by ${5:sorry}"
],
"description": "Scaffolding for authoring `calc` blocks"
},
Expand Down

0 comments on commit ad8305e

Please sign in to comment.