rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 14 Pull Requests Releases Wiki Activity

tiny tweak

This commit is contained in:
rhiannon morris 2022-05-25 16:03:23 +02:00
parent 818d559d58
commit 2b756ae1bb
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Quox/Syntax/Term/Base.idr
View File

@ -90,8 +90,8 @@ mutual
%name DScopeTerm body
public export %inline
Arr : Qty -> Term d n -> Term d n -> Term d n
Arr pi a b = Pi {qty = pi, x = "_", arg = a, res = TUnused b}
Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
||| same as `F` but as a term
public export %inline