Stream: Coq users

Topic: meaning of following command

view this post on Zulip pianke (May 01 2023 at 06:37):

apply iff_trans with (1 := existsb_exists _ _).

view this post on Zulip Laurent Théry (May 01 2023 at 07:43):

It instanciates the first argument of iff_trans with existsb_exists before applying it : 

Require Import List.

Check  iff_trans.
(* First argument A <-> B*)
Check existsb_exists.
Check (@iff_trans _ _ _ (@existsb_exists _ _ _)).

Last updated: Oct 13 2024 at 01:02 UTC