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

give some subterms better names

Browse source
This commit is contained in:
rhiannon morris 2021-09-03 16:32:22 +02:00
parent bc1aa21f09
commit e03b4a4286
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -36,17 +36,17 @@ mutual
||| function type
Pi : (qty, qtm : Qty) -> (x : Name) ->
(a : Term d n) -> (b : Term d (S n)) -> Term d n
(arg : Term d n) -> (res : Term d (S n)) -> Term d n
||| function term
Lam : (x : Name) -> (t : Term d (S n)) -> Term d n
Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
||| elimination
E : (e : Elim d n) -> Term d n
||| term closure/suspended substitution
CloT : (s : Term d from) -> (th : Lazy (TSubst d from to)) -> Term d to
CloT : (tm : Term d from) -> (th : Lazy (TSubst d from to)) -> Term d to
||| dimension closure/suspended substitution
DCloT : (s : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
||| first argument `d` is dimension scope size, second `n` is term scope size
public export
@ -57,15 +57,15 @@ mutual
B : (i : Var n) -> Elim d n
||| term application
(:@) : (f : Elim d n) -> (s : Term d n) -> Elim d n
(:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
||| type-annotated term
(:#) : (s, a : Term d n) -> Elim d n
(:#) : (tm, ty : Term d n) -> Elim d n
||| term closure/suspended substitution
CloE : (e : Elim d from) -> (th : Lazy (TSubst d from to)) -> Elim d to
CloE : (el : Elim d from) -> (th : Lazy (TSubst d from to)) -> Elim d to
||| dimension closure/suspended substitution
DCloE : (e : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
%name Term s, t, r
%name Elim e, f
@ -323,8 +323,8 @@ parameters {auto _ : Alternative f}
||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
export
betaLam1 : Elim d n -> f (Elim d n)
betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) =
pure $ (t :# b) // (s :# a ::: id)
betaLam1 ((Lam {body, _} :# Pi {arg, res, _}) :@ s) =
pure $ (body :# res) // (s :# arg ::: id)
betaLam1 _ = empty
||| `(e ⦂ A) >>> e` [if `e` is an elim]