Jules Bean wrote:
Been playing and, well... it's amazing stuff. Here are the problems I've run into:
* as constructor declarations, nil:List X and (----------! are inequivalent, strangely (?) !nil:List X)
nil : List X is not (syntactically) a constructor declaration. The 2nd version is correct.
* in
( X : * ! ( xs : List X ; x : X ! data !------------! where (--------------! ; !----------------------! ! List X : * ) ! nil : List X ) ! cons x xs : List X )
The order of x and xs above the line is significant.
Precisely.
As it stands, it
won't elaborate. Replace the top line with x:X ; xs:List X and it will. I have seen other similar problems requiring me to reorder things to get it to elaborate.
Just declare the domain types in the order they are applied.
* If you define a function type without dummy arguments (i.e. plus: Nat -> Nat -> Nat instead of plus x y : Nat) then I can't work out how to write the program interactively. I tried "lam x <= case x" but that didn't work... (shoudl there be a new 'abstr' strategy for defining by lambda abstraction?)
They are not dummy arguments, by writing down the template of the function you also indicate which parameters are explicit and which are implicit, i.e. to be inferred. If you write no arguments Epigram thinks they are all implicit but in this case will be unable to infer them.
I.e. nil is a good example: if you write nil X above instead of nil you always have to supply the type when using nil.
That's the obvious things. I also can't get a non-trivial instance of the 'oh So true' trick to work, but that might be operator error, or it might just been you haven't written enough of the proof search code yet.
What is "a non-trivial instance of the 'oh So true' trick"?
Cheers, Thorsten
-- Dr. Thorsten Altenkirch phone : (+44) (0)115 84 66516 Lecturer http://www.cs.nott.ac.uk/~txa/ School of Computer Science & IT University of Nottingham
This message has been scanned but we cannot guarantee that it and any attachments are free from viruses or other damaging content: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
