Commit 6ad60b3c authored by Katja Bercic's avatar Katja Bercic

Update notation in the DbData theory

parent d862d61f
......@@ -93,21 +93,21 @@ theory DbData : ur:?PLF =
db_uuid : db_tp❙
db_array : db_tp ⟶ db_tp❙
eq : {a} V a ⟶ V a ⟶ V db_bool❙
neq : {a} V a ⟶ V a ⟶ V db_bool❙
eq : {a} V a ⟶ V a ⟶ V db_bool❘# 1 = 2
neq : {a} V a ⟶ V a ⟶ V db_bool❘# 1 != 2
leq : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 2❙
leq : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 <= 2❙
lt : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 < 2❙
geq : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 2❙
geq : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 >= 2❙
gt : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 > 2❙
elemAt : {a} V db_array a ⟶ V db_int ⟶ V a❙
length : {a} V db_array a ⟶ V db_int❙
lengthDim: {a} V db_array a ⟶ V db_int ⟶ V db_int❙
contains : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❙
containedIn : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❙
hasCommonElem : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❙
contains : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❘# 1 @> 2
containedIn : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❘# 1 <@ 2
hasCommonElem : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❘# 1 && 2
theory Codecs : ur:?PLF =
......
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