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

more ScopeTerm stuff

Browse source
This commit is contained in:
rhiannon morris 2022-04-09 18:54:47 +02:00
parent 4722e144a3
commit 46b29b8e72
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Quox.idr
View file

@ -26,7 +26,7 @@ banner = #"""
export export
tm : Term 1 2 tm : Term 1 2
tm = tm =
(Pi Zero One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"])) (Pi Zero One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
`DCloT` (K One ::: id)) `DCloT` (K One ::: id))
`CloT` (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id) `CloT` (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)

10
src/Quox/Equal.idr
View file

@ -46,12 +46,12 @@ parameters {auto _ : MonadThrow Error m}
eq ClashQ qtm1 qtm2 eq ClashQ qtm1 qtm2
eq ClashQ qty1 qty2 eq ClashQ qty1 qty2
equalT0 arg1 arg2 equalT0 arg1 arg2
equalT0 res1 res2 equalTS0 res1 res2
equalTN' s@(Pi {}) t _ _ = clashT s t equalTN' s@(Pi {}) t _ _ = clashT s t
-- [todo] eta -- [todo] eta
equalTN' (Lam _ body1) (Lam _ body2) _ _ = equalTN' (Lam _ body1) (Lam _ body2) _ _ =
equalT0 body1 body2 equalTS0 body1 body2
equalTN' s@(Lam {}) t _ _ = clashT s t equalTN' s@(Lam {}) t _ _ = clashT s t
equalTN' (E e) (E f) ps pt = equalE0 e f equalTN' (E e) (E f) ps pt = equalE0 e f
@ -113,3 +113,9 @@ parameters {auto _ : MonadThrow Error m}
export covering %inline export covering %inline
equalE0 : Elim 0 n -> Elim 0 n -> m () equalE0 : Elim 0 n -> Elim 0 n -> m ()
equalE0 e f = whnfE e `equalEN` whnfE f equalE0 e f = whnfE e `equalEN` whnfE f
export covering %inline
equalTS0 : ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
equalTS0 (TUnused body1) (TUnused body2) = equalT0 body1 body2
equalTS0 body1 body2 =
fromScopeTerm body1 `equalT0` fromScopeTerm body2