formatting fixes & tweaks

This commit is contained in:
rhiannon morris 2021-09-03 17:10:50 +02:00
parent d41ab0897c
commit 6c05a348d5
2 changed files with 3 additions and 3 deletions

View File

@ -52,7 +52,7 @@ public export
public export
CanSubst Var Var where
i // Shift by = shift by i
i // Shift by = shift by i
VZ // (t ::: th) = t
VS i // (t ::: th) = i // th

View File

@ -295,7 +295,7 @@ mutual
pushSubstsT' th ph (Lam x t) =
Element (Lam x $ subs t th $ push ph) Oh
pushSubstsT' th ph (E e) =
case pushSubstsE' th ph e of Element e' prf => Element (E e') prf
let Element e prf = pushSubstsE' th ph e in Element (E e) prf
pushSubstsT' th ph (CloT s ps) =
pushSubstsT' th (comp' th ps ph) s
pushSubstsT' th ph (DCloT s ps) =
@ -319,7 +319,7 @@ mutual
parameters {auto _ : Alternative f}
||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)]`
export
betaLam1 : Elim d n -> f (Elim d n)
betaLam1 ((Lam {body, _} :# Pi {arg, res, _}) :@ s) =