blob: 856e05fe5275c3c7500e96702eba0a51624dfccb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
postulate TypeData : Set 1
postulate Value : (type : TypeData) -> Set
postulate Equality : (left : TypeData) -> (right : TypeData) -> Prop
postulate Cast :
(oldType : TypeData) ->
(newType : TypeData) ->
(equality : Equality oldType newType) ->
(value : Value oldType) ->
Value newType
postulate EqualityCorrect :
(left : TypeData) ->
(right : TypeData) ->
Equality left right ~ (Value left ~ Value right)
postulate CastCorrect :
(oldType : TypeData) ->
(newType : TypeData) ->
(equality : Equality oldType newType) ->
(value : Value oldType) ->
Cast oldType newType equality value ~
cast (Value oldType) (Value newType) (fst (EqualityCorrect oldType newType) equality) value
|
