blob: 19a8408689c51ea1716c87affcf7d23c99ddfe89 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
TypeData : Prop
TypeData = ()
Value : (type : TypeData) -> Set 1
Value = \type => Set
Equality : (left : TypeData) -> (right : TypeData) -> Prop
Equality = \left => \right => ()
Cast :
(oldType : TypeData) ->
(newType : TypeData) ->
(equality : Equality oldType newType) ->
(value : Value oldType) ->
Value newType
Cast = \oldType => \newType => \equality => \value => value
EqualityCorrect :
(left : TypeData) ->
(right : TypeData) ->
Equality left right ~ (Value left ~ Value right)
EqualityCorrect = refl Equality
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
CastCorrect = refl Cast
|
