On Sat, Jun 13, 2015 at 6:11 AM, Keean Schupke <[email protected]> wrote: > On 13 June 2015 at 10:47, Matt Oliveri <[email protected]> wrote: >> It may not be worth explaining it yet. There are still simpler things, >> like HasTwo, and even10, that I'm waiting for you to address. > > I can't find a reference to HasTwo, but even10: > >> Inductive Even : nat->Prop := >> ez : Even O | >> ess n : Even n->Even (S (S n)). >> Definition even10 : Even 10 := ess 8 (ess 6 (ess 4 (ess 2 (ess 0 ez)))). > > > I don't really get what you want me to do here? > > > The type level logic program: > > nat(z). > nat(s(X)) :- nat(X). > > even(z). > even(s(s(X))) :- even(X). > > :- even(s(s(s(s(s(s(s(s(s(s(z))))))))))). > yes.
That's about what I was expecting. > So given a value level program: > > ten :: even a => a > ten = 10 > > this works because '10' has the type s(s(s(s(s(s(s(s(s(s(z)))))))))) as it > is a literal. Ah, you've anticipated one of my follow-up questions! So it looks like you _are_ doing something like Habit. Why didn't you say so? Does this work? add2 :: even a => even b => a -> b add2 x = x + 2 The terms getting types a and b are not literals, but thinking of those types as singletons, this example still makes sense. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
