@@ -135,41 +135,41 @@ instance heytingAlgebraRecordCons
135135 => HeytingAlgebraRecord (RL.Cons key focus rowlistTail ) row subrow where
136136 conjRecord _ ra rb = insert (conj (get ra) (get rb)) tail
137137 where
138- key = reflectSymbol (SProxy :: SProxy key )
138+ key = reflectSymbol (Proxy :: Proxy key )
139139 get = unsafeGet key :: Record row -> focus
140140 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
141141 tail = conjRecord (Proxy :: Proxy rowlistTail ) ra rb
142142
143143 disjRecord _ ra rb = insert (disj (get ra) (get rb)) tail
144144 where
145- key = reflectSymbol (SProxy :: SProxy key )
145+ key = reflectSymbol (Proxy :: Proxy key )
146146 get = unsafeGet key :: Record row -> focus
147147 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
148148 tail = disjRecord (Proxy :: Proxy rowlistTail ) ra rb
149149
150150 impliesRecord _ ra rb = insert (implies (get ra) (get rb)) tail
151151 where
152- key = reflectSymbol (SProxy :: SProxy key )
152+ key = reflectSymbol (Proxy :: Proxy key )
153153 get = unsafeGet key :: Record row -> focus
154154 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
155155 tail = impliesRecord (Proxy :: Proxy rowlistTail ) ra rb
156156
157157 ffRecord _ row = insert ff tail
158158 where
159- key = reflectSymbol (SProxy :: SProxy key )
159+ key = reflectSymbol (Proxy :: Proxy key )
160160 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
161161 tail = ffRecord (Proxy :: Proxy rowlistTail ) row
162162
163163 notRecord _ row
164164 = insert (not (get row)) tail
165165 where
166- key = reflectSymbol (SProxy :: SProxy key )
166+ key = reflectSymbol (Proxy :: Proxy key )
167167 get = unsafeGet key :: Record row -> focus
168168 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
169169 tail = notRecord (Proxy :: Proxy rowlistTail ) row
170170
171171 ttRecord _ row = insert tt tail
172172 where
173- key = reflectSymbol (SProxy :: SProxy key )
173+ key = reflectSymbol (Proxy :: Proxy key )
174174 insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
175175 tail = ttRecord (Proxy :: Proxy rowlistTail ) row
0 commit comments