rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

remove a noLoc

Browse source
This commit is contained in:
rhiannon morris 2023-06-11 19:25:38 +02:00
parent 865772d512
commit cd330c1092
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
lib/Quox/Syntax/Term/Subst.idr
View file

@ -334,8 +334,7 @@ private %inline
CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
CompHY {ty, p, q, val, r, zero, one, loc} = CompHY {ty, p, q, val, r, zero, one, loc} =
-- [fixme] maintain location of existing B VZ let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
let ty' = SY ty.names $ ty.term // (B VZ noLoc ::: shift 2) in
Comp { Comp {
ty = dsub1 ty q, p, q, ty = dsub1 ty q, p, q,
val = E $ Coe ty p q val val.loc, r, val = E $ Coe ty p q val val.loc, r,