Skip to content

GitLab

Commit f6891785 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Expr and Obj where redundant

parent 7861eb68
Hide whitespace changes
Inline Side-by-side
dk_obj.dk
View file @ f6891785
......@@ -118,22 +118,16 @@ preupdate : A : ObjType ->
(Po_cons A f D l2 m2 o)
(Po_cons A f D l1 m1 (preupdate A f D o l2 m2)).
Obj : ObjType -> Type.
[ A : ObjType ]
Obj A
-->
PreObj A (Ot_assoc A) (Ot_domain A).
make : A : ObjType -> Obj A -> Expr A.
[ A : ObjType ] expr A --> preObj A (Ot_assoc A) (Ot_domain A).
select : A : ObjType ->
eA : Expr A ->
l : Label ->
Expr (Ot_assoc A l).
[ A : ObjType,
o : Obj A,
o : Expr A,
l : Label ]
select A (make _ o) l
select A o l
-->
preselect
A
......@@ -141,7 +135,7 @@ select : A : ObjType ->
(Ot_domain A)
o
l
(make A o).
o.
update : A : ObjType ->
eA : Expr A ->
......@@ -149,20 +143,18 @@ update : A : ObjType ->
(Expr A -> Expr (Ot_assoc A l)) ->
Expr A.
[A : ObjType,
o : Obj A,
o : Expr A,
l : Label,
m : Expr A -> Expr (Ot_assoc A l)]
update A (make _ o) l m
update A o l m
-->
make
preupdate
A
(preupdate
A
(Ot_assoc A)
(Ot_domain A)
o
l
m).
(Ot_assoc A)
(Ot_domain A)
o
l
m.
(; Subtyping ;)
......@@ -285,7 +277,7 @@ preinit : A : ObjType ->
init : A : ObjType -> Expr A
:= A : ObjType =>
make A (preinit A (Ot_domain A)).
preinit A (Ot_domain A).
coerce : A : ObjType ->
B : ObjType ->
......@@ -297,12 +289,11 @@ coerce : A : ObjType ->
B : ObjType =>
H : Istrue (Ot_st A B) =>
o : Expr A =>
make B
(Ot_eq_po
B
A
B
(Ot_domain B)
(l : Label =>
Ot_assoc_subtype A B l H)
(ocast A B o)).
Ot_eq_po
B
A
B
(Ot_domain B)
(l : Label =>
Ot_assoc_subtype A B l H)
(ocast A B o).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment