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

Comments

parent cc687fd9
...@@ -197,6 +197,10 @@ obj_select : A : ObjType -> ...@@ -197,6 +197,10 @@ obj_select : A : ObjType ->
H H
o. o.
(; The definitions of select and update
are limited to objects so that selection
and updating other expressions is still definable. ;)
select : A : ObjType -> select : A : ObjType ->
eA : Expr A -> eA : Expr A ->
l : Label -> l : Label ->
...@@ -267,8 +271,6 @@ mem_update := A : ObjType => ...@@ -267,8 +271,6 @@ mem_update := A : ObjType =>
H : Istrue (dk_domain.mem l (Ot_domain A)) => H : Istrue (dk_domain.mem l (Ot_domain A)) =>
update A eA l (dk_domain.mem_pos l (Ot_domain A) H). update A eA l (dk_domain.mem_pos l (Ot_domain A) H).
(; Subtyping ;)
preinit : A : ObjType -> preinit : A : ObjType ->
C : Domain -> C : Domain ->
Hsub : dk_domain.Subset C (Ot_domain A) -> Hsub : dk_domain.Subset C (Ot_domain A) ->
...@@ -297,6 +299,8 @@ init : A : ObjType -> Expr A ...@@ -297,6 +299,8 @@ init : A : ObjType -> Expr A
:= A : ObjType => := A : ObjType =>
preinit A (Ot_domain A) (l : Label => H : domain_pos l (Ot_domain A) => H). preinit A (Ot_domain A) (l : Label => H : domain_pos l (Ot_domain A) => H).
(; Subtyping ;)
eq_coerce : A : ObjType -> eq_coerce : A : ObjType ->
B : ObjType -> B : ObjType ->
Istrue (Ot_eq A B) -> Istrue (Ot_eq A B) ->
......
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