User loginNavigation |
archivesEncoding System Fw in predicative dependent type theorySystem Fω appears impredicative, but I'm wondering if there is an easy way to embed it into predicative dependent type theory by inferring bounds on universes. Also, if anyone can provide an example of a System Fω term that would be rejected by Coq's typical ambiguity resolver, that would be helpful to me. Any references or thought are appreciated. Predicates, ghost predicates and higher order predicatesThis short article describes how predicates are handled in Modern Eiffel. In a similar manner as with functions(described in Functions ... ), predicates can be ghost predicates and/or higher order predicates. By hbrandl at 2012-05-17 19:27 | LtU Forum | login or register to post comments | other blogs | 5260 reads
|
Browse archivesActive forum topics
|
Recent comments
11 weeks 1 day ago
15 weeks 3 days ago
17 weeks 15 hours ago
17 weeks 15 hours ago
19 weeks 5 days ago
24 weeks 2 days ago
24 weeks 2 days ago
24 weeks 5 days ago
24 weeks 5 days ago
27 weeks 4 days ago