Stream: MetaCoq

Topic: Notation tProd Anon ?


view this post on Zulip Thomas Lamiaux (May 12 2024 at 17:20):

Hi, I am using MetaCoq to generates types, and I often have to generate non dependent function types. Would there be a notation like A -> B for tProp "Anon" A B ?

view this post on Zulip Théo Winterhalter (May 13 2024 at 01:06):

I thought there was.

view this post on Zulip Théo Winterhalter (May 13 2024 at 01:07):

I can't find it. But it probably wouldn't print most of the time because it would require a lift in B.

view this post on Zulip Théo Winterhalter (May 13 2024 at 01:08):

I see that one in examples: https://github.com/MetaCoq/metacoq/blob/coq-8.17/examples/typing_correctness.v#L87

view this post on Zulip Théo Winterhalter (May 13 2024 at 01:09):

So I guess it's not defined in the core library.

view this post on Zulip Thomas Lamiaux (May 13 2024 at 06:23):

Ok, I'll define something my development thanks

view this post on Zulip Yann Leray (May 13 2024 at 08:53):

It's also here now


Last updated: Jul 23 2024 at 20:01 UTC