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

wap quantities in pi to match grtt

Browse source
This commit is contained in:
rhiannon morris 2021-12-23 19:03:37 +01:00
parent b5cfc7b23b
commit 730cedc4c0
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -34,7 +34,7 @@ mutual
TYPE : (l : Universe) -> Term d n TYPE : (l : Universe) -> Term d n
||| function type ||| function type
Pi : (qty, qtm : Qty) -> (x : Name) -> Pi : (qtm, qty : Qty) -> (x : Name) ->
(arg : Term d n) -> (res : Term d (S n)) -> Term d n (arg : Term d n) -> (res : Term d (S n)) -> Term d n
||| function term ||| function term
Lam : (x : Name) -> (body : Term d (S n)) -> Term d n Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
@ -126,9 +126,9 @@ mutual
PrettyHL (Term d n) where PrettyHL (Term d n) where
prettyM (TYPE l) = prettyM (TYPE l) =
parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l) parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
prettyM (Pi qty qtm x s t) = prettyM (Pi qtm qty x s t) =
parensIfM Outer $ hang 2 $ parensIfM Outer $ hang 2 $
!(prettyBinder [qty, qtm] x s) <++> !arrowD !(prettyBinder [qtm, qty] x s) <++> !arrowD
<//> !(under T x $ prettyM t) <//> !(under T x $ prettyM t)
prettyM (Lam x t) = prettyM (Lam x t) =
parensIfM Outer $ parensIfM Outer $
@ -320,8 +320,8 @@ mutual
Term dfrom from -> NotCloTerm dto to Term dfrom from -> NotCloTerm dto to
pushSubstsTWith th ph (TYPE l) = pushSubstsTWith th ph (TYPE l) =
ncloT $ TYPE l ncloT $ TYPE l
pushSubstsTWith th ph (Pi qty qtm x a b) = pushSubstsTWith th ph (Pi qtm qty x a b) =
ncloT $ Pi qty qtm x (subs a th ph) (subs b th (push ph)) ncloT $ Pi qtm qty x (subs a th ph) (subs b th (push ph))
pushSubstsTWith th ph (Lam x t) = pushSubstsTWith th ph (Lam x t) =
ncloT $ Lam x $ subs t th $ push ph ncloT $ Lam x $ subs t th $ push ph
pushSubstsTWith th ph (E e) = pushSubstsTWith th ph (E e) =