Skip to content

Commit

Permalink
fix(tactic/core): correct of_int doc string (#1671)
Browse files Browse the repository at this point in the history
  • Loading branch information
robertylewis authored and mergify[bot] committed Nov 11, 2019
1 parent 6ecdefc commit a5b3af3
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/tactic/core.lean
Expand Up @@ -19,7 +19,7 @@ nat.binary_rec
do e ← tac, tactic.mk_app (cond b ``bit1 ``bit0) [e])

/-- Given an expr `α` representing a type with numeral structure,
`of_nat α n` creates the `α`-valued numeral expression corresponding to `n`.
`of_int α n` creates the `α`-valued numeral expression corresponding to `n`.
The output is either a numeral or the negation of a numeral. -/
protected meta def of_int (α : expr) : ℤ → tactic expr
| (n : ℕ) := expr.of_nat α n
Expand Down

0 comments on commit a5b3af3

Please sign in to comment.