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

add parameters block a constraint

Browse source
This commit is contained in:
rhiannon morris 2021-09-03 15:00:43 +02:00
parent 3c411aca83
commit f592e2e3dc
1 changed files with 15 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/Quox/Syntax/Term.idr
View file

@ -319,22 +319,23 @@ mutual
pushSubstsE' (ps . th) ph e pushSubstsE' (ps . th) ph e
||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)` parameters {auto _ : Alternative f}
export ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
betaLam1 : Alternative f => Elim d n -> f (Elim d n) export
betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) = betaLam1 : Elim d n -> f (Elim d n)
pure $ (t :# b) // (s :# a ::: id) betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) =
betaLam1 _ = empty pure $ (t :# b) // (s :# a ::: id)
betaLam1 _ = empty
||| `(e ⦂ A) >>> e` [if `e` is an elim] ||| `(e ⦂ A) >>> e` [if `e` is an elim]
export export
upsilon1 : Alternative f => Elim d n -> f (Elim d n) upsilon1 : Elim d n -> f (Elim d n)
upsilon1 (E e :# _) = pure e upsilon1 (E e :# _) = pure e
upsilon1 _ = empty upsilon1 _ = empty
public export public export
step : Alternative f => Elim d n -> f (Elim d n) step : Elim d n -> f (Elim d n)
step e = betaLam1 e <|> upsilon1 e step e = betaLam1 e <|> upsilon1 e
public export public export
step' : Elim d n -> Elim d n step' : Elim d n -> Elim d n