[Agda] subset types? refinement types? type synonyms? type
abbreviations?
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Nov 10 22:40:56 CET 2011
Hello Ramana,
> Also, I am indexing terms by whether or not they are a variable (as
> well as by their type); I use that information for the Abs
> constructor.
I would not do it like that. Rather have a separate type of variables,
data Var : Type -> Set
and then
data Term : Type -> Set where
var : {t : Type} -> Var t -> Term t
...
abs : {t u : Type} -> Var t -> Term u -> Term (t => u)
Or even better, use some flavor of nameless term representation. You
see a lot of approaches advertized in the later messages of the threat
"Associativity for free!".
> How can I define Formula?
>
> Formula : Bool -> Set
> Formula = Term bool
I am confused, didn't you just define Formula? It is a Term of type
bool, that's it.
Cheers,
Andreas
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list