haveIdLhs'

Mathlib.Tactic.Have

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.haveIdLhs'

Lean4

/-- Uses `checkColGt` to prevent

```lean
have h
exact Nat
```

From being interpreted as
```lean
have h
  exact Nat
```
-/
def haveIdLhs' : Parser :=
  optBinderIdent >> many (ppSpace >> checkColGt "expected to be indented" >> letIdBinder) >> optType

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru