@@ -97,12 +97,12 @@ instance heytingAlgebraProxy3 :: HeytingAlgebra (Proxy3 a) where
9797 tt = Proxy3
9898
9999instance heytingAlgebraRecord :: (RL.RowToList row list , HeytingAlgebraRecord list row row ) => HeytingAlgebra (Record row ) where
100- ff = ffRecord (RLProxy :: RLProxy list ) (RProxy :: RProxy row )
101- tt = ttRecord (RLProxy :: RLProxy list ) (RProxy :: RProxy row )
102- conj = conjRecord (RLProxy :: RLProxy list )
103- disj = disjRecord (RLProxy :: RLProxy list )
104- implies = impliesRecord (RLProxy :: RLProxy list )
105- not = notRecord (RLProxy :: RLProxy list )
100+ ff = ffRecord (Proxy :: Proxy list ) (RProxy :: RProxy row )
101+ tt = ttRecord (Proxy :: Proxy list ) (RProxy :: RProxy row )
102+ conj = conjRecord (Proxy :: Proxy list )
103+ disj = disjRecord (Proxy :: Proxy list )
104+ implies = impliesRecord (Proxy :: Proxy list )
105+ not = notRecord (Proxy :: Proxy list )
106106
107107foreign import boolConj :: Boolean -> Boolean -> Boolean
108108foreign import boolDisj :: Boolean -> Boolean -> Boolean
@@ -138,38 +138,38 @@ instance heytingAlgebraRecordCons
138138 key = reflectSymbol (SProxy :: SProxy key )
139139 get = unsafeGet key :: Record row -> focus
140140 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
141- tail = conjRecord (RLProxy :: RLProxy rowlistTail ) ra rb
141+ tail = conjRecord (Proxy :: Proxy rowlistTail ) ra rb
142142
143143 disjRecord _ ra rb = insert (disj (get ra) (get rb)) tail
144144 where
145145 key = reflectSymbol (SProxy :: SProxy key )
146146 get = unsafeGet key :: Record row -> focus
147147 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
148- tail = disjRecord (RLProxy :: RLProxy rowlistTail ) ra rb
148+ tail = disjRecord (Proxy :: Proxy rowlistTail ) ra rb
149149
150150 impliesRecord _ ra rb = insert (implies (get ra) (get rb)) tail
151151 where
152152 key = reflectSymbol (SProxy :: SProxy key )
153153 get = unsafeGet key :: Record row -> focus
154154 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
155- tail = impliesRecord (RLProxy :: RLProxy rowlistTail ) ra rb
155+ tail = impliesRecord (Proxy :: Proxy rowlistTail ) ra rb
156156
157157 ffRecord _ row = insert ff tail
158158 where
159159 key = reflectSymbol (SProxy :: SProxy key )
160160 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
161- tail = ffRecord (RLProxy :: RLProxy rowlistTail ) row
161+ tail = ffRecord (Proxy :: Proxy rowlistTail ) row
162162
163163 notRecord _ row
164164 = insert (not (get row)) tail
165165 where
166166 key = reflectSymbol (SProxy :: SProxy key )
167167 get = unsafeGet key :: Record row -> focus
168168 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
169- tail = notRecord (RLProxy :: RLProxy rowlistTail ) row
169+ tail = notRecord (Proxy :: Proxy rowlistTail ) row
170170
171171 ttRecord _ row = insert tt tail
172172 where
173173 key = reflectSymbol (SProxy :: SProxy key )
174174 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
175- tail = ttRecord (RLProxy :: RLProxy rowlistTail ) row
175+ tail = ttRecord (Proxy :: Proxy rowlistTail ) row
0 commit comments