max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove coe functions

Browse source 
They will be used in the new `Coe` file
This commit is contained in:
Leonardo de Moura 2020-01-28 08:49:02 -08:00
parent 5083ecffcc
commit ef105ba49d
1 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Coe.lean
View file

@ -73,15 +73,6 @@ HasCoeToFun.coe
@[reducible, inline] def oldCoeSort {a : Sort u} [HasCoeToSort.{u, v} a] : a → HasCoeToSort.S.{u, v} a :=
HasCoeToSort.coe
@[reducible, inline] def coe {a : Sort u} {b : Sort v} [HasLiftT a b] : a → b :=
liftT
@[reducible, inline] def coeFn {a : Sort u} [HasCoeToFun.{u, v} a] : ∀ (x : a), HasCoeToFun.F.{u, v} x :=
HasCoeToFun.coe
@[reducible, inline] def coeSort {a : Sort u} [HasCoeToSort.{u, v} a] : a → HasCoeToSort.S.{u, v} a :=
HasCoeToSort.coe
/- Notation -/
universes u₁ u₂ u₃