Idris2/tests/idris2/linear016/Issue2895.idr

record Ty where
  constructor MkTy
  0 obj : Type

record TyProj (d: Ty) where
  constructor MkTyProj
  proj : d.obj

record Id (x : Type) where
  constructor MkId
  getId : x

DepLensToDepOptic :
  {c1 : TyProj (MkTy (Nat -> Type))} ->
  Id (proj c1 3) -> -- remove the Id works
  Type
DepLensToDepOptic (MkId b') = ?hu
add tests 2023-02-25 15:19:29 +03:00			`record Ty where`
			`constructor MkTy`
			`0 obj : Type`

			`record TyProj (d: Ty) where`
			`constructor MkTyProj`
			`proj : d.obj`

			`record Id (x : Type) where`
			`constructor MkId`
			`getId : x`

			`DepLensToDepOptic :`
			`{c1 : TyProj (MkTy (Nat -> Type))} ->`
add logs to linear check 2023-02-25 21:40:21 +03:00			`Id (proj c1 3) -> -- remove the Id works`
add tests 2023-02-25 15:19:29 +03:00			`Type`
			`DepLensToDepOptic (MkId b') = ?hu`