refactor(library): remove all instances of `(...)
This commit is contained in:
parent
b3975c8fc1
commit
171a96a8de
2 changed files with 3 additions and 3 deletions
|
|
@ -427,10 +427,10 @@ meta def generalize2 (p : parse qexpr) (x : parse ident) (h : parse ident) : tac
|
|||
do tgt ← target,
|
||||
e ← to_expr p,
|
||||
let e' := tgt^.replace $ λa _, if a = e then some (var 1) else none,
|
||||
to_expr `(Π x, %%p = x → %%e') >>= assert h,
|
||||
to_expr ``(Π x, %%p = x → %%e') >>= assert h,
|
||||
swap,
|
||||
t ← get_local h,
|
||||
exact `(%%t %%p rfl),
|
||||
exact ``(%%t %%p rfl),
|
||||
intro x,
|
||||
intro h
|
||||
|
||||
|
|
|
|||
|
|
@ -120,7 +120,7 @@ do env ← get_env,
|
|||
new_goal ← to_expr ``(∀ (_idx : %%I_idx_type), decidable_eq (%%I_basic_const _idx)),
|
||||
assert `_basic_dec_eq new_goal,
|
||||
swap,
|
||||
to_expr `(_basic_dec_eq %%I_idx) >>= exact,
|
||||
`[exact _basic_dec_eq %%I_idx],
|
||||
intro1,
|
||||
return () },
|
||||
mk_dec_eq_instance_core
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue