ssreflect - Re: [ssreflect] Dependent cast 'Z_p -> 'F_p

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Dependent cast 'Z_p -> 'F_p

From: Florent Hivert <>
To: georges gonthier <>
Cc: "" <>
Subject: Re: [ssreflect] Dependent cast 'Z_p -> 'F_p
Date: Thu, 26 Sep 2019 18:51:27 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:QOL9SxBYrsVXPKv6CYCiUyQJP3N1i/DPJgcQr6AfoPdwSPv8o8bcNUDSrc9gkEXOFd2Cra4d0KyN7+u5ATFIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfL1/IA+4oAjeucUanJduJ6YswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKLCAy/n3JhcNsjaJbuBOhqAJ5w47Ie4GeKf5ycrrAcd8GWWZNW8BcXDFDDIyhdYsCF+QPM+ZGoYfgpFUOoxSxChWxC+ztxDBGiWT73bEj0+g9DQ3KwBYtEtAIvX/JrNv1LqASUeWtwafIyTXDaOlW1in76IjUbxsvo/CMXaxufsrL1UkkCgTIgFWUqYziJTOayOINs3SB4+RiVOKvlXAoqxttojW0wscskIjJipgbylDe7Ch0xps+K96gSENjfNKoDp9duzuHO4Z0Qs4uWXxktSYgxrEbpZK2ejUBxo49yB7FcfOHdpCF4hL9W+aVJjd1nHdld6i+hxa270ehxfH8WtOw0FZQrypJiNfMtmoV2xzS7MiIVOd981+81TqR0w3f8PxILEI0mKbBNpIswqQ8mocPvUjbGy/5gkT2jKuYdkU+/eio7vzqbLXipp+bLY97lAf+Mrg0lsK9AOQ4LBYBX3KH+emn0L3j50z5TK9Ejv0siqXZqozVJdwHpq6lBA9Yyp0j6w2lDzi43tQYmWcII05ZeB+clIjoO1TOIOjiAvulglSsli1rx/HcMbH7DJXNNCuLrLC0crt68UFR00I8ytZD55NZEPlVL//0QED8r5rXCRklMw252c7mDs9838UQQzTcLLWeNfb8tViS6+Qza8mNeoIPpH6pBfwi/fPokTkZmEEQZ7WB2YEWLn6iSKc1a36FaGbh149SWVwBuRAzGamz0AXbAGxjIk2qVqd53QkVTYevDIPNXIeo0O6Fxib9EIcEPzkbWGDJKm/hcsC/Y9lJaC+WJZY/wDkNVLysW5Nn0Quv8gHgmeI+crjkvxYAvJem7+BbovXJnEFg8SZ1ScqHgTmA

On Thu, Sep 26, 2019 at 01:09:27PM +0200, georges gonthier wrote:
> If you really want to be selective, then note that indeed ‘Z_p does not
> appear in the goal because Ltac erases type casts, so only the structures
> inferred from ‘Z_p will actually appear in the goal.

Thanks for the explanation ! I didn't know that. That's why I got confused.

Best,

Florent

[ssreflect] Dependent cast 'Z_p -> 'F_p, Florent Hivert, 09/26/2019
- Re: [ssreflect] Dependent cast 'Z_p -> 'F_p, Laurent Thery, 09/26/2019
  - Re: [ssreflect] Dependent cast 'Z_p -> 'F_p, georges gonthier, 09/26/2019
  - Re: [ssreflect] Dependent cast 'Z_p -> 'F_p, Florent Hivert, 09/26/2019
    - Re: [ssreflect] Dependent cast 'Z_p -> 'F_p, Laurent Thery, 09/26/2019
    - Re: [ssreflect] Dependent cast 'Z_p -> 'F_p, georges gonthier, 09/26/2019
      - Re: [ssreflect] Dependent cast 'Z_p -> 'F_p, Florent Hivert, 09/26/2019

List archive

Re: [ssreflect] Dependent cast 'Z_p -> 'F_p