search

namme-anetten / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

Code review: making AllowedBy in Tactics.Data #64

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
The AllowedBy data-type is defined by:

AllowedBy : Set -> Set
AllowedBy Ty = Sigma ['epsilon 'cons] 
                     ['Const Unit
                     , 'Sigma Set $ \ S ->
                       'Sigma (S -> Set) $ \ T ->
                       'Sigma (:- Ty == (x : S) -> T) $ \ _ ->
                       'Sigma S $ \ s ->
                       'Sigma (AllowedBy (T s)) $ \ _ ->
                       'Const Unit ]

So, on 'cons, we have to give a proof that the S-T we give are equal to Ty. In 
Tactics.Data, I have hopefully given the right things to 'cons. Then, for the 
proof, I have simply given refl. 

Is that correct?

Original issue reported on code.google.com by pedag...@gmail.com on 29 Aug 2010 at 1:33