Skip to content

Commit 35c393d

Browse files
LinyxusLinyxus
committed
replace all <- with \lto 
1 parent 5ee0180 commit 35c393d

File tree

3 files changed

+24
-24
lines changed

3 files changed

+24
-24
lines changed

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -43,15 +43,15 @@ structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where
4343
def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.rename f) where
4444
var := fun x P hb => by
4545
cases hb
46-
case here => simp only [<-Ty.rename_succVar_comm]; constructor
46+
case here => simp only [←Ty.rename_succVar_comm]; constructor
4747
case there_var hb =>
48-
simp only [<-Ty.rename_succVar_comm]
48+
simp only [←Ty.rename_succVar_comm]
4949
constructor
5050
apply ρ.var _ _ hb
5151
tvar := fun X S hb => by
5252
cases hb
5353
case there_var hb =>
54-
simp only [<-Ty.rename_succVar_comm]
54+
simp only [←Ty.rename_succVar_comm]
5555
constructor
5656
apply ρ.tvar _ _ hb
5757

@@ -62,14 +62,14 @@ def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.r
6262
def Rebind.liftTVar (ρ : Rebind Γ f Δ) : Rebind (Γ,X<:T) (f.liftTVar) (Δ,X<:T.rename f) where
6363
tvar := fun X S hb => by
6464
cases hb
65-
case here => simp only [<-Ty.rename_succTVar_comm]; constructor
65+
case here => simp only [←Ty.rename_succTVar_comm]; constructor
6666
case there_tvar hb =>
67-
simp only [<-Ty.rename_succTVar_comm]
67+
simp only [←Ty.rename_succTVar_comm]
6868
constructor
6969
apply ρ.tvar _ _ hb
7070
var := fun x P hb => by
7171
cases hb
72-
case there_tvar hb => simp only [<-Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb
72+
case there_tvar hb => simp only [←Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb
7373

7474
/-- **Term variable weakening morphism**.
7575

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -40,17 +40,17 @@ def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P
4040
cases hb
4141
case here =>
4242
apply HasType.var
43-
simp only [<-Ty.subst_succVar_comm_base]
43+
simp only [←Ty.subst_succVar_comm_base]
4444
constructor
4545
case there_var hb0 =>
4646
have h0 := ρ.var _ _ hb0
47-
simp only [<-Ty.subst_succVar_comm_base]
47+
simp only [←Ty.subst_succVar_comm_base]
4848
apply h0.rebind Rebind.succVar
4949
tvar := fun X S hb => by
5050
cases hb
5151
case there_var hb0 =>
5252
have h0 := ρ.tvar _ _ hb0
53-
simp only [<-Ty.subst_succVar_comm_base]
53+
simp only [←Ty.subst_succVar_comm_base]
5454
apply h0.rebind Rebind.succVar
5555

5656
/-- Extends a retyping morphism to contexts with an additional type variable. -/
@@ -59,7 +59,7 @@ def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ,
5959
cases hb
6060
case there_tvar hb0 =>
6161
have h0 := ρ.var _ _ hb0
62-
simp only [<-Ty.subst_succTVar_comm_base]
62+
simp only [←Ty.subst_succTVar_comm_base]
6363
apply h0.rebind Rebind.succTVar
6464
tvar := fun X S hb => by
6565
cases hb
@@ -68,7 +68,7 @@ def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ,
6868
grind [Ty.subst_succTVar_comm_base]
6969
case there_tvar hb0 =>
7070
have h0 := ρ.tvar _ _ hb0
71-
simp only [<-Ty.subst_succTVar_comm_base]
71+
simp only [←Ty.subst_succTVar_comm_base]
7272
apply h0.rebind Rebind.succTVar
7373

7474
/-- Creates a retyping morphism that substitutes an expression for the newest term variable. -/

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -48,14 +48,14 @@ theorem Ty.tvar_subst_succVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) :
4848
simp only [Subst.lift, Ty.subst]
4949
conv => lhs; simp only [Subst.liftVar]
5050
conv => rhs; simp only [Subst.tvar_there_var_liftVar]
51-
simp only [Rename.lift, <-Ty.rename_succVar_comm]
51+
simp only [Rename.lift, ←Ty.rename_succVar_comm]
5252
congr; exact (ih (X:=X0))
5353
case push_tvar s0 ih =>
5454
cases X <;> try rfl
5555
case there_tvar X0 =>
5656
conv => lhs; simp only [Subst.lift, Ty.subst]
5757
conv => lhs; simp only [Subst.liftTVar, Rename.lift]
58-
simp only [<-Ty.rename_succTVar_comm]
58+
simp only [←Ty.rename_succTVar_comm]
5959
congr; exact (ih (X:=X0))
6060

6161
/-- Proves that substitution commutes with type variable weakening for type variables. -/
@@ -69,14 +69,14 @@ theorem Ty.tvar_subst_succTVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) :
6969
case there_var X0 =>
7070
conv => lhs; simp only [Subst.lift, Ty.subst]
7171
conv => lhs; simp only [Subst.liftVar, Rename.lift]
72-
simp only [<-Ty.rename_succVar_comm]
72+
simp only [←Ty.rename_succVar_comm]
7373
congr; exact (ih (X:=X0))
7474
case push_tvar s0 ih =>
7575
cases X <;> try rfl
7676
case there_tvar X0 =>
7777
conv => lhs; simp only [Subst.lift, Ty.subst]
7878
conv => lhs; simp only [Subst.liftTVar, Rename.lift]
79-
simp only [<-Ty.rename_succTVar_comm]
79+
simp only [←Ty.rename_succTVar_comm]
8080
congr; exact (ih (X:=X0))
8181

8282
/-- Proves that substitution commutes with term variable weakening for types. -/
@@ -143,14 +143,14 @@ theorem Exp.var_subst_succTVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) :
143143
case there_var x0 =>
144144
conv => lhs; simp only [Subst.lift, Exp.subst]
145145
conv => lhs; simp only [Subst.liftVar, Rename.lift]
146-
simp only [<-Exp.rename_succVar_comm]
146+
simp only [←Exp.rename_succVar_comm]
147147
congr; exact (ih (x:=x0))
148148
case push_tvar s0 ih =>
149149
cases x
150150
case there_tvar x0 =>
151151
conv => lhs; simp only [Subst.liftVar, Subst.lift, Rename.lift]
152152
conv => lhs; simp only [Exp.subst, Subst.liftTVar]
153-
simp only [<-Exp.rename_succTVar_comm]
153+
simp only [←Exp.rename_succTVar_comm]
154154
congr; exact (ih (x:=x0))
155155

156156
/-- Proves that substitution commutes with term variable weakening for variables. -/
@@ -162,13 +162,13 @@ theorem Exp.var_subst_succVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) :
162162
cases x <;> try rfl
163163
case there_var x0 =>
164164
conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftVar, Rename.lift]
165-
simp only [<-Exp.rename_succVar_comm]
165+
simp only [←Exp.rename_succVar_comm]
166166
congr; exact (ih (x:=x0))
167167
case push_tvar s0 ih =>
168168
cases x
169169
case there_tvar x0 =>
170170
conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftTVar, Rename.lift]
171-
simp only [<-Exp.rename_succTVar_comm]
171+
simp only [←Exp.rename_succTVar_comm]
172172
congr; exact (ih (x:=x0))
173173

174174
/-- Proves that substitution commutes with type variable weakening for expressions. -/
@@ -330,7 +330,7 @@ theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} :
330330
/-- Proves that opening a type variable commutes with renaming for types. -/
331331
theorem Ty.open_tvar_rename_comm {T : Ty (s,X)} {U : Ty s} {f : Rename s s'} :
332332
(T.open_tvar U).rename f = (T.rename f.liftTVar).open_tvar (U.rename f) := by
333-
simp [Ty.open_tvar, <-Ty.subst_asSubst]
333+
simp [Ty.open_tvar, ←Ty.subst_asSubst]
334334
grind [Ty.subst_comp, Subst.open_tvar_rename_comm, Ty.subst_asSubst]
335335

336336
/-- Shows that successively weakening then opening a type variable gives the identity. -/
@@ -341,14 +341,14 @@ theorem Subst.succTVar_open_tvar {T : Ty s} :
341341
theorem Exp.rename_succTVar_open_tvar {e : Exp s} :
342342
(e.rename Rename.succTVar).subst (Subst.open_tvar X) =
343343
e := by
344-
simp [<-Exp.subst_asSubst]
344+
simp [←Exp.subst_asSubst]
345345
grind [Exp.subst_comp, Subst.succTVar_open_tvar, Exp.subst_id]
346346

347347
/-- Proves that renaming with succTVar then opening cancels out for types. -/
348348
theorem Ty.rename_succTVar_open_tvar {T : Ty s} :
349349
(T.rename Rename.succTVar).subst (Subst.open_tvar X) =
350350
T := by
351-
simp [<-Ty.subst_asSubst]
351+
simp [←Ty.subst_asSubst]
352352
grind [Ty.subst_comp, Subst.succTVar_open_tvar, Ty.subst_id]
353353

354354
/-- Shows that successively weakening then opening a term variable gives the identity. -/
@@ -359,14 +359,14 @@ theorem Subst.succVar_open_var {e : Exp s} :
359359
theorem Exp.rename_succVar_open_var {e : Exp s} :
360360
(e.rename Rename.succVar).subst (Subst.open_var X) =
361361
e := by
362-
simp [<-Exp.subst_asSubst]
362+
simp [←Exp.subst_asSubst]
363363
grind [Exp.subst_comp, Subst.succVar_open_var, Exp.subst_id]
364364

365365
/-- Proves that renaming with succVar then opening cancels out for types. -/
366366
theorem Ty.rename_succVar_open_var {T : Ty s} :
367367
(T.rename Rename.succVar).subst (Subst.open_var X) =
368368
T := by
369-
simp [<-Ty.subst_asSubst]
369+
simp [←Ty.subst_asSubst]
370370
grind [Ty.subst_comp, Subst.succVar_open_var, Ty.subst_id]
371371

372372
/-- Proves that opening a type variable commutes with substitution for substitutions. -/

0 commit comments

Comments
 (0)