chore: Remove redundant code
This commit is contained in:
parent
b9ff9e8f13
commit
91fbc4cdca
|
@ -207,8 +207,6 @@ def test_env_add_inspect : Test :=
|
||||||
Protocol.EnvInspectResult),
|
Protocol.EnvInspectResult),
|
||||||
]
|
]
|
||||||
|
|
||||||
def f.{u} : (α : Type u) → α → (α × α) := λ (α : Type u) (x : α) => (x, x)
|
|
||||||
|
|
||||||
example : ∀ (p: Prop), p → p := by
|
example : ∀ (p: Prop), p → p := by
|
||||||
intro p h
|
intro p h
|
||||||
exact h
|
exact h
|
||||||
|
|
Loading…
Reference in New Issue