@@ -8,6 +8,8 @@ import Prelude.Functor
88import Prelude.List
99import Prelude.Nat
1010import Prelude.Traversable
11+import Prelude.Uninhabited
12+import Decidable.Equality
1113
1214%access public export
1315
@@ -24,7 +26,25 @@ record SourceLocation where
2426 ||| The line and column of the end of the source span
2527 end : (Int, Int)
2628
27−%name SourceLocation loc
29+%name SourceLocation loc, loc'
30+
31+private
32+fileLocInj : (FileLoc fn s e = FileLoc fn' s' e') -> (fn = fn', s = s', e = e')
33+fileLocInj Refl = (Refl, Refl, Refl)
34+
35+implementation DecEq SourceLocation where
36+ decEq (FileLoc f s e) (FileLoc f' s' e') with (decEq f f')
37+ decEq (FileLoc f s e) (FileLoc f s' e') | Yes Refl with (decEq s s')
38+ decEq (FileLoc f s e) (FileLoc f s e') | Yes Refl | Yes Refl with (decEq e e')
39+ decEq (FileLoc f s e) (FileLoc f s e) | Yes Refl | Yes Refl | Yes Refl =
40+ Yes Refl
41+ decEq (FileLoc f s e) (FileLoc f s e') | Yes Refl | Yes Refl | No contra =
42+ No $ contra . snd . snd . fileLocInj
43+ decEq (FileLoc f s e) (FileLoc f s' e') | Yes Refl | No contra =
44+ No $ contra . fst . snd . fileLocInj
45+ decEq (FileLoc f s e) (FileLoc f' s' e') | No contra =
46+ No $ contra . fst . fileLocInj
47+
2848
2949
3050mutual
@@ -52,12 +72,504 @@ mutual
5272 | ElimN TTName
5373 | InstanceCtorN TTName
5474 | MetaN TTName TTName
75+ %name SpecialName sn, sn'
76+
77+-- Rather than implement one-off private functions, we make the
78+-- disjointness of the constructors available to all Idris programs,
79+-- at the cost of a bit of scrolling here.
80+
81+implementation Uninhabited (UN _ = NS _ _) where
82+ uninhabited Refl impossible
83+
84+implementation Uninhabited (UN _ = MN _ _) where
85+ uninhabited Refl impossible
86+
87+implementation Uninhabited (UN _ = SN _) where
88+ uninhabited Refl impossible
89+
90+implementation Uninhabited (NS _ _ = UN _) where
91+ uninhabited Refl impossible
92+
93+implementation Uninhabited (NS _ _ = MN _ _) where
94+ uninhabited Refl impossible
95+
96+implementation Uninhabited (NS _ _ = SN _) where
97+ uninhabited Refl impossible
98+
99+implementation Uninhabited (MN _ _ = UN _) where
100+ uninhabited Refl impossible
101+
102+implementation Uninhabited (MN _ _ = NS _ _) where
103+ uninhabited Refl impossible
104+
105+implementation Uninhabited (MN _ _ = SN _) where
106+ uninhabited Refl impossible
107+
108+implementation Uninhabited (SN _ = UN _) where
109+ uninhabited Refl impossible
110+
111+implementation Uninhabited (SN _ = MN _ _) where
112+ uninhabited Refl impossible
113+
114+implementation Uninhabited (SN _ = NS _ _) where
115+ uninhabited Refl impossible
116+
117+implementation Uninhabited ((WhereN x n n') = (WithN y z)) where
118+ uninhabited Refl impossible
119+
120+implementation Uninhabited ((WhereN x n n') = (InstanceN y xs)) where
121+ uninhabited Refl impossible
122+
123+implementation Uninhabited ((WhereN x n n') = (ParentN y z)) where
124+ uninhabited Refl impossible
125+
126+implementation Uninhabited ((WhereN x n n') = (MethodN y)) where
127+ uninhabited Refl impossible
128+
129+implementation Uninhabited ((WhereN x n n') = (CaseN loc y)) where
130+ uninhabited Refl impossible
131+
132+implementation Uninhabited ((WhereN x n n') = (ElimN y)) where
133+ uninhabited Refl impossible
134+
135+implementation Uninhabited ((WhereN x n n') = (InstanceCtorN y)) where
136+ uninhabited Refl impossible
137+
138+implementation Uninhabited ((WhereN x n n') = (MetaN y z)) where
139+ uninhabited Refl impossible
140+
141+implementation Uninhabited ((WithN x n) = (WhereN y n' z)) where
142+ uninhabited Refl impossible
143+
144+implementation Uninhabited ((WithN x n) = (InstanceN n' xs)) where
145+ uninhabited Refl impossible
146+
147+implementation Uninhabited ((WithN x n) = (ParentN n' y)) where
148+ uninhabited Refl impossible
149+
150+implementation Uninhabited ((WithN x n) = (MethodN n')) where
151+ uninhabited Refl impossible
152+
153+implementation Uninhabited ((WithN x n) = (CaseN loc n')) where
154+ uninhabited Refl impossible
155+
156+implementation Uninhabited ((WithN x n) = (ElimN n')) where
157+ uninhabited Refl impossible
158+
159+implementation Uninhabited ((WithN x n) = (InstanceCtorN n')) where
160+ uninhabited Refl impossible
161+
162+implementation Uninhabited ((WithN x n) = (MetaN n' y)) where
163+ uninhabited Refl impossible
164+
165+implementation Uninhabited ((InstanceN n xs) = (WhereN x n' y)) where
166+ uninhabited Refl impossible
167+
168+implementation Uninhabited ((InstanceN n xs) = (WithN x n')) where
169+ uninhabited Refl impossible
170+
171+implementation Uninhabited ((InstanceN n xs) = (ParentN n' x)) where
172+ uninhabited Refl impossible
173+
174+implementation Uninhabited ((InstanceN n xs) = (MethodN n')) where
175+ uninhabited Refl impossible
176+
177+implementation Uninhabited ((InstanceN n xs) = (CaseN loc n')) where
178+ uninhabited Refl impossible
179+
180+implementation Uninhabited ((InstanceN n xs) = (ElimN n')) where
181+ uninhabited Refl impossible
182+
183+implementation Uninhabited ((InstanceN n xs) = (InstanceCtorN n')) where
184+ uninhabited Refl impossible
185+
186+implementation Uninhabited ((InstanceN n xs) = (MetaN n' x)) where
187+ uninhabited Refl impossible
188+
189+implementation Uninhabited ((ParentN n x) = (WhereN y n' z)) where
190+ uninhabited Refl impossible
191+
192+implementation Uninhabited ((ParentN n x) = (WithN y n')) where
193+ uninhabited Refl impossible
194+
195+implementation Uninhabited ((ParentN n x) = (InstanceN n' xs)) where
196+ uninhabited Refl impossible
197+
198+implementation Uninhabited ((ParentN n x) = (MethodN n')) where
199+ uninhabited Refl impossible
55200
201+implementation Uninhabited ((ParentN n x) = (CaseN loc n')) where
202+ uninhabited Refl impossible
56203
204+implementation Uninhabited ((ParentN n x) = (ElimN n')) where
205+ uninhabited Refl impossible
57206
58−implicit
59−userSuppliedName : String -> TTName
60−userSuppliedName = UN
207+implementation Uninhabited ((ParentN n x) = (InstanceCtorN n')) where
208+ uninhabited Refl impossible
209+
210+implementation Uninhabited ((ParentN n x) = (MetaN n' y)) where
211+ uninhabited Refl impossible
212+
213+implementation Uninhabited ((MethodN n) = (WhereN x n' y)) where
214+ uninhabited Refl impossible
215+
216+implementation Uninhabited ((MethodN n) = (WithN x n')) where
217+ uninhabited Refl impossible
218+
219+implementation Uninhabited ((MethodN n) = (InstanceN n' xs)) where
220+ uninhabited Refl impossible
221+
222+implementation Uninhabited ((MethodN n) = (ParentN n' x)) where
223+ uninhabited Refl impossible
224+
225+implementation Uninhabited ((MethodN n) = (CaseN loc n')) where
226+ uninhabited Refl impossible
227+
228+implementation Uninhabited ((MethodN n) = (ElimN n')) where
229+ uninhabited Refl impossible
230+
231+implementation Uninhabited ((MethodN n) = (InstanceCtorN n')) where
232+ uninhabited Refl impossible
233+
234+implementation Uninhabited ((MethodN n) = (MetaN n' x)) where
235+ uninhabited Refl impossible
236+
237+implementation Uninhabited ((CaseN loc n) = (WhereN x n' y)) where
238+ uninhabited Refl impossible
239+
240+implementation Uninhabited ((CaseN loc n) = (WithN x n')) where
241+ uninhabited Refl impossible
242+
243+implementation Uninhabited ((CaseN loc n) = (InstanceN n' xs)) where
244+ uninhabited Refl impossible
245+
246+implementation Uninhabited ((CaseN loc n) = (ParentN n' x)) where
247+ uninhabited Refl impossible
248+
249+implementation Uninhabited ((CaseN loc n) = (MethodN n')) where
250+ uninhabited Refl impossible
251+
252+implementation Uninhabited ((CaseN loc n) = (ElimN n')) where
253+ uninhabited Refl impossible
254+
255+implementation Uninhabited ((CaseN loc n) = (InstanceCtorN n')) where
256+ uninhabited Refl impossible
257+
258+implementation Uninhabited ((CaseN loc n) = (MetaN n' x)) where
259+ uninhabited Refl impossible
260+
261+implementation Uninhabited ((ElimN n) = (WhereN x n' y)) where
262+ uninhabited Refl impossible
263+
264+implementation Uninhabited ((ElimN n) = (WithN x n')) where
265+ uninhabited Refl impossible
266+
267+implementation Uninhabited ((ElimN n) = (InstanceN n' xs)) where
268+ uninhabited Refl impossible
269+
270+implementation Uninhabited ((ElimN n) = (ParentN n' x)) where
271+ uninhabited Refl impossible
272+
273+implementation Uninhabited ((ElimN n) = (MethodN n')) where
274+ uninhabited Refl impossible
275+
276+implementation Uninhabited ((ElimN n) = (CaseN loc n')) where
277+ uninhabited Refl impossible
278+
279+implementation Uninhabited ((ElimN n) = (InstanceCtorN n')) where
280+ uninhabited Refl impossible
281+
282+implementation Uninhabited ((ElimN n) = (MetaN n' x)) where
283+ uninhabited Refl impossible
284+
285+implementation Uninhabited ((InstanceCtorN n) = (WhereN x n' y)) where
286+ uninhabited Refl impossible
287+
288+implementation Uninhabited ((InstanceCtorN n) = (WithN x n')) where
289+ uninhabited Refl impossible
290+
291+implementation Uninhabited ((InstanceCtorN n) = (InstanceN n' xs)) where
292+ uninhabited Refl impossible
293+
294+implementation Uninhabited ((InstanceCtorN n) = (ParentN n' x)) where
295+ uninhabited Refl impossible
296+
297+implementation Uninhabited ((InstanceCtorN n) = (MethodN n')) where
298+ uninhabited Refl impossible
299+
300+implementation Uninhabited ((InstanceCtorN n) = (CaseN loc n')) where
301+ uninhabited Refl impossible
302+
303+implementation Uninhabited ((InstanceCtorN n) = (ElimN n')) where
304+ uninhabited Refl impossible
305+
306+implementation Uninhabited ((InstanceCtorN n) = (MetaN n' x)) where
307+ uninhabited Refl impossible
308+
309+implementation Uninhabited ((MetaN n n') = (WhereN x y z)) where
310+ uninhabited Refl impossible
311+
312+implementation Uninhabited ((MetaN n n') = (WithN x y)) where
313+ uninhabited Refl impossible
314+
315+implementation Uninhabited ((MetaN n n') = (InstanceN x xs)) where
316+ uninhabited Refl impossible
317+
318+implementation Uninhabited ((MetaN n n') = (ParentN x y)) where
319+ uninhabited Refl impossible
320+
321+implementation Uninhabited ((MetaN n n') = (MethodN x)) where
322+ uninhabited Refl impossible
323+
324+implementation Uninhabited ((MetaN n n') = (CaseN loc x)) where
325+ uninhabited Refl impossible
326+
327+implementation Uninhabited ((MetaN n n') = (ElimN x)) where
328+ uninhabited Refl impossible
329+
330+implementation Uninhabited ((MetaN n n') = (InstanceCtorN x)) where
331+ uninhabited Refl impossible
332+
333+mutual
334+ private
335+ unInj : (UN x = UN y) -> x = y
336+ unInj Refl = Refl
337+
338+ private
339+ nsInj : (NS n ns = NS n' ns') -> (n = n', ns = ns')
340+ nsInj Refl = (Refl, Refl)
341+
342+ private
343+ mnInj : (MN i s = MN i' s') -> (i = i', s = s')
344+ mnInj Refl = (Refl, Refl)
345+
346+ private
347+ snInj : SN sn = SN sn' -> sn = sn'
348+ snInj Refl = Refl
349+
350+ private
351+ decTTNameEq : (n1, n2 : TTName) -> Dec (n1 = n2)
352+ decTTNameEq (UN x) (UN y) with (decEq x y)
353+ decTTNameEq (UN x) (UN y) | Yes prf =
354+ Yes (cong prf)
355+ decTTNameEq (UN x) (UN y) | No contra =
356+ No $ contra . unInj
357+ decTTNameEq (UN x) (NS n xs) = No absurd
358+ decTTNameEq (UN x) (MN y z) = No absurd
359+ decTTNameEq (UN x) (SN y) = No absurd
360+ decTTNameEq (NS n xs) (UN x) = No absurd
361+ decTTNameEq (NS n ns) (NS n' ns') with (decTTNameEq n n')
362+ decTTNameEq (NS n ns) (NS n ns') | Yes Refl with (decEq ns ns')
363+ decTTNameEq (NS n ns) (NS n ns) | Yes Refl | Yes Refl =
364+ Yes Refl
365+ decTTNameEq (NS n ns) (NS n ns') | Yes Refl | No contra =
366+ No $ contra . snd . nsInj
367+ decTTNameEq (NS n ns) (NS n' ns') | No contra =
368+ No $ contra . fst . nsInj
369+ decTTNameEq (NS n xs) (MN x y) = No absurd
370+ decTTNameEq (NS n xs) (SN x) = No absurd
371+ decTTNameEq (MN x y) (UN z) = No absurd
372+ decTTNameEq (MN x y) (NS n xs) = No absurd
373+ decTTNameEq (MN x y) (MN z w) with (decEq x z)
374+ decTTNameEq (MN x y) (MN x w) | Yes Refl with (decEq y w)
375+ decTTNameEq (MN x y) (MN x y) | Yes Refl | Yes Refl =
376+ Yes Refl
377+ decTTNameEq (MN x y) (MN x w) | Yes Refl | No contra =
378+ No $ contra . snd . mnInj
379+ decTTNameEq (MN x y) (MN z w) | No contra =
380+ No $ contra . fst . mnInj
381+ decTTNameEq (MN x y) (SN z) = No absurd
382+ decTTNameEq (SN x) (UN y) = No absurd
383+ decTTNameEq (SN x) (NS n xs) = No absurd
384+ decTTNameEq (SN x) (MN y z) = No absurd
385+ decTTNameEq (SN x) (SN y) with (decSNEq x y)
386+ decTTNameEq (SN x) (SN x) | Yes Refl = Yes Refl
387+ decTTNameEq (SN x) (SN y) | (No contra) = No $ contra . snInj
388+
389+
390+ private
391+ whereNInj : (WhereN x n n' = WhereN y z w) -> (x = y, n = z, n' = w)
392+ whereNInj Refl = (Refl, Refl, Refl)
393+
394+ private
395+ withNInj : (WithN x n = WithN y n') -> (x = y, n = n')
396+ withNInj Refl = (Refl, Refl)
397+
398+ private
399+ instanceNInj : (InstanceN n xs = InstanceN n' ys) -> (n = n', xs = ys)
400+ instanceNInj Refl = (Refl, Refl)
401+
402+ private
403+ parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y)
404+ parentNInj Refl = (Refl, Refl)
405+
406+ private
407+ methodNInj : (MethodN n = MethodN n') -> n = n'
408+ methodNInj Refl = Refl
409+
410+ private
411+ caseNInj : (CaseN loc n = CaseN loc' n') -> (loc = loc', n = n')
412+ caseNInj Refl = (Refl, Refl)
413+
414+ private
415+ elimNInj : (ElimN n = ElimN n') -> n = n'
416+ elimNInj Refl = Refl
417+
418+ private
419+ instanceCtorNInj : (InstanceCtorN n = InstanceCtorN n') -> n = n'
420+ instanceCtorNInj Refl = Refl
421+
422+ private
423+ metaNInj : (MetaN n m = MetaN n' m') -> (n = n', m = m')
424+ metaNInj Refl = (Refl, Refl)
425+
426+ private
427+ decSNEq : (n1, n2 : SpecialName) -> Dec (n1 = n2)
428+ decSNEq (WhereN x n n') (WhereN y z w) with (decEq x y)
429+ decSNEq (WhereN x n n') (WhereN x z w) | Yes Refl with (assert_total $ decTTNameEq n z)
430+ decSNEq (WhereN x n n') (WhereN x n w) | Yes Refl | Yes Refl with (assert_total $ decTTNameEq n' w)
431+ decSNEq (WhereN x n n') (WhereN x n n') | Yes Refl | Yes Refl | Yes Refl =
432+ Yes Refl
433+ decSNEq (WhereN x n n') (WhereN x n w) | Yes Refl | Yes Refl | No contra =
434+ No $ contra . snd . snd . whereNInj
435+ decSNEq (WhereN x n n') (WhereN x z w) | Yes Refl | No contra =
436+ No $ contra . fst . snd . whereNInj
437+ decSNEq (WhereN x n n') (WhereN y z w) | No contra =
438+ No $ contra . fst . whereNInj
439+ decSNEq (WhereN x n n') (WithN y z) = No absurd
440+ decSNEq (WhereN x n n') (InstanceN y xs) = No absurd
441+ decSNEq (WhereN x n n') (ParentN y z) = No absurd
442+ decSNEq (WhereN x n n') (MethodN y) = No absurd
443+ decSNEq (WhereN x n n') (CaseN loc y) = No absurd
444+ decSNEq (WhereN x n n') (ElimN y) = No absurd
445+ decSNEq (WhereN x n n') (InstanceCtorN y) = No absurd
446+ decSNEq (WhereN x n n') (MetaN y z) = No absurd
447+ decSNEq (WithN x n) (WhereN y n' z) = No absurd
448+ decSNEq (WithN x n) (WithN y n') with (decEq x y)
449+ decSNEq (WithN x n) (WithN x n') | Yes Refl with (assert_total $ decTTNameEq n n')
450+ decSNEq (WithN x n) (WithN x n) | Yes Refl | Yes Refl =
451+ Yes Refl
452+ decSNEq (WithN x n) (WithN x n') | Yes Refl | No contra =
453+ No $ contra . snd . withNInj
454+ decSNEq (WithN x n) (WithN y n') | No contra =
455+ No $ contra . fst . withNInj
456+ decSNEq (WithN x n) (InstanceN n' xs) = No absurd
457+ decSNEq (WithN x n) (ParentN n' y) = No absurd
458+ decSNEq (WithN x n) (MethodN n') = No absurd
459+ decSNEq (WithN x n) (CaseN loc n') = No absurd
460+ decSNEq (WithN x n) (ElimN n') = No absurd
461+ decSNEq (WithN x n) (InstanceCtorN n') = No absurd
462+ decSNEq (WithN x n) (MetaN n' y) = No absurd
463+ decSNEq (InstanceN n xs) (WhereN x n' y) = No absurd
464+ decSNEq (InstanceN n xs) (WithN x n') = No absurd
465+ decSNEq (InstanceN n xs) (InstanceN n' ys) with (assert_total $ decTTNameEq n n')
466+ decSNEq (InstanceN n xs) (InstanceN n ys) | Yes Refl with (decEq xs ys)
467+ decSNEq (InstanceN n xs) (InstanceN n xs) | Yes Refl | Yes Refl =
468+ Yes Refl
469+ decSNEq (InstanceN n xs) (InstanceN n ys) | Yes Refl | No contra =
470+ No $ contra . snd . instanceNInj
471+ decSNEq (InstanceN n xs) (InstanceN n' ys) | No contra =
472+ No $ contra . fst . instanceNInj
473+ decSNEq (InstanceN n xs) (ParentN n' x) = No absurd
474+ decSNEq (InstanceN n xs) (MethodN n') = No absurd
475+ decSNEq (InstanceN n xs) (CaseN loc n') = No absurd
476+ decSNEq (InstanceN n xs) (ElimN n') = No absurd
477+ decSNEq (InstanceN n xs) (InstanceCtorN n') = No absurd
478+ decSNEq (InstanceN n xs) (MetaN n' x) = No absurd
479+ decSNEq (ParentN n x) (WhereN y n' z) = No absurd
480+ decSNEq (ParentN n x) (WithN y n') = No absurd
481+ decSNEq (ParentN n x) (InstanceN n' xs) = No absurd
482+ decSNEq (ParentN n x) (ParentN n' y) with (assert_total $ decTTNameEq n n')
483+ decSNEq (ParentN n x) (ParentN n y) | Yes Refl with (decEq x y)
484+ decSNEq (ParentN n x) (ParentN n x) | Yes Refl | Yes Refl =
485+ Yes Refl
486+ decSNEq (ParentN n x) (ParentN n y) | Yes Refl | No contra =
487+ No $ contra . snd . parentNInj
488+ decSNEq (ParentN n x) (ParentN n' y) | No contra =
489+ No $ contra . fst . parentNInj
490+ decSNEq (ParentN n x) (MethodN n') = No absurd
491+ decSNEq (ParentN n x) (CaseN loc n') = No absurd
492+ decSNEq (ParentN n x) (ElimN n') = No absurd
493+ decSNEq (ParentN n x) (InstanceCtorN n') = No absurd
494+ decSNEq (ParentN n x) (MetaN n' y) = No absurd
495+ decSNEq (MethodN n) (WhereN x n' y) = No absurd
496+ decSNEq (MethodN n) (WithN x n') = No absurd
497+ decSNEq (MethodN n) (InstanceN n' xs) = No absurd
498+ decSNEq (MethodN n) (ParentN n' x) = No absurd
499+ decSNEq (MethodN n) (MethodN n') with (assert_total $ decTTNameEq n n')
500+ decSNEq (MethodN n) (MethodN n) | Yes Refl =
501+ Yes Refl
502+ decSNEq (MethodN n) (MethodN n') | No contra =
503+ No $ contra . methodNInj
504+ decSNEq (MethodN n) (CaseN loc n') = No absurd
505+ decSNEq (MethodN n) (ElimN n') = No absurd
506+ decSNEq (MethodN n) (InstanceCtorN n') = No absurd
507+ decSNEq (MethodN n) (MetaN n' x) = No absurd
508+ decSNEq (CaseN loc n) (WhereN x n' y) = No absurd
509+ decSNEq (CaseN loc n) (WithN x n') = No absurd
510+ decSNEq (CaseN loc n) (InstanceN n' xs) = No absurd
511+ decSNEq (CaseN loc n) (ParentN n' x) = No absurd
512+ decSNEq (CaseN loc n) (MethodN n') = No absurd
513+ decSNEq (CaseN loc n) (CaseN loc' n') with (decEq loc loc')
514+ decSNEq (CaseN loc n) (CaseN loc n') | Yes Refl with (assert_total $ decTTNameEq n n')
515+ decSNEq (CaseN loc n) (CaseN loc n) | Yes Refl | Yes Refl =
516+ Yes Refl
517+ decSNEq (CaseN loc n) (CaseN loc n') | Yes Refl | No contra =
518+ No $ contra . snd . caseNInj
519+ decSNEq (CaseN loc n) (CaseN loc' n') | No contra =
520+ No $ contra . fst . caseNInj
521+ decSNEq (CaseN loc n) (ElimN n') = No absurd
522+ decSNEq (CaseN loc n) (InstanceCtorN n') = No absurd
523+ decSNEq (CaseN loc n) (MetaN n' x) = No absurd
524+ decSNEq (ElimN n) (WhereN x n' y) = No absurd
525+ decSNEq (ElimN n) (WithN x n') = No absurd
526+ decSNEq (ElimN n) (InstanceN n' xs) = No absurd
527+ decSNEq (ElimN n) (ParentN n' x) = No absurd
528+ decSNEq (ElimN n) (MethodN n') = No absurd
529+ decSNEq (ElimN n) (CaseN loc n') = No absurd
530+ decSNEq (ElimN n) (ElimN n') with (assert_total $ decTTNameEq n n')
531+ decSNEq (ElimN n) (ElimN n) | Yes Refl =
532+ Yes Refl
533+ decSNEq (ElimN n) (ElimN n') | No contra =
534+ No $ contra . elimNInj
535+ decSNEq (ElimN n) (InstanceCtorN n') = No absurd
536+ decSNEq (ElimN n) (MetaN n' x) = No absurd
537+ decSNEq (InstanceCtorN n) (WhereN x n' y) = No absurd
538+ decSNEq (InstanceCtorN n) (WithN x n') = No absurd
539+ decSNEq (InstanceCtorN n) (InstanceN n' xs) = No absurd
540+ decSNEq (InstanceCtorN n) (ParentN n' x) = No absurd
541+ decSNEq (InstanceCtorN n) (MethodN n') = No absurd
542+ decSNEq (InstanceCtorN n) (CaseN loc n') = No absurd
543+ decSNEq (InstanceCtorN n) (ElimN n') = No absurd
544+ decSNEq (InstanceCtorN n) (InstanceCtorN n') with (assert_total $ decTTNameEq n n')
545+ decSNEq (InstanceCtorN n) (InstanceCtorN n) | Yes Refl =
546+ Yes Refl
547+ decSNEq (InstanceCtorN n) (InstanceCtorN n') | No contra =
548+ No $ contra . instanceCtorNInj
549+ decSNEq (InstanceCtorN n) (MetaN n' x) = No absurd
550+ decSNEq (MetaN n n') (WhereN x y z) = No absurd
551+ decSNEq (MetaN n n') (WithN x y) = No absurd
552+ decSNEq (MetaN n n') (InstanceN x xs) = No absurd
553+ decSNEq (MetaN n n') (ParentN x y) = No absurd
554+ decSNEq (MetaN n n') (MethodN x) = No absurd
555+ decSNEq (MetaN n n') (CaseN loc x) = No absurd
556+ decSNEq (MetaN n n') (ElimN x) = No absurd
557+ decSNEq (MetaN n n') (InstanceCtorN x) = No absurd
558+ decSNEq (MetaN n n') (MetaN x y) with (assert_total $ decTTNameEq n x)
559+ decSNEq (MetaN n n') (MetaN n y) | Yes Refl with (assert_total $ decTTNameEq n' y)
560+ decSNEq (MetaN n n') (MetaN n n') | Yes Refl | Yes Refl =
561+ Yes Refl
562+ decSNEq (MetaN n n') (MetaN n y) | Yes Refl | No contra =
563+ No $ contra . snd . metaNInj
564+ decSNEq (MetaN n n') (MetaN x y) | No contra =
565+ No $ contra . fst . metaNInj
566+
567+
568+implementation DecEq TTName where
569+ decEq = decTTNameEq
570+
571+implementation DecEq SpecialName where
572+ decEq = decSNEq
61573
62574data TTUExp =
63575 ||| Universe variable