Documentation

Init.Guard

Reducible defeq matching for guard_hyp types

Equations
    Instances For

      Default-reducibility defeq matching for guard_hyp types

      Equations
        Instances For

          Syntactic matching for guard_hyp types

          Equations
            Instances For

              Alpha-eq matching for guard_hyp types

              Equations
                Instances For

                  The guard_hyp type specifier, one of :, :~, :ₛ, :ₐ

                  Equations
                    Instances For

                      Reducible defeq matching for guard_hyp values

                      Equations
                        Instances For

                          Default-reducibility defeq matching for guard_hyp values

                          Equations
                            Instances For

                              Syntactic matching for guard_hyp values

                              Equations
                                Instances For

                                  Alpha-eq matching for guard_hyp values

                                  Equations
                                    Instances For

                                      The guard_hyp value specifier, one of :=, :=~, :=ₛ, :=ₐ

                                      Equations
                                        Instances For

                                          Reducible defeq matching for guard_expr

                                          Equations
                                            Instances For

                                              Default-reducibility defeq matching for guard_expr

                                              Equations
                                                Instances For

                                                  Syntactic matching for guard_expr

                                                  Equations
                                                    Instances For

                                                      Alpha-eq matching for guard_expr

                                                      Equations
                                                        Instances For

                                                          The guard_expr matching specifier, one of =, =~, =ₛ, =ₐ

                                                          Equations
                                                            Instances For

                                                              Tactic to check equality of two expressions.

                                                              • guard_expr e = e' checks that e and e' are defeq at reducible transparency.
                                                              • guard_expr e =~ e' checks that e and e' are defeq at default transparency.
                                                              • guard_expr e =ₛ e' checks that e and e' are syntactically equal.
                                                              • guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

                                                              Both e and e' are elaborated then have their metavariables instantiated before the equality check. Their types are unified (using isDefEqGuarded) before synthetic metavariables are processed, which helps with default instance handling.

                                                              Equations
                                                                Instances For

                                                                  Tactic to check equality of two expressions.

                                                                  • guard_expr e = e' checks that e and e' are defeq at reducible transparency.
                                                                  • guard_expr e =~ e' checks that e and e' are defeq at default transparency.
                                                                  • guard_expr e =ₛ e' checks that e and e' are syntactically equal.
                                                                  • guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

                                                                  Both e and e' are elaborated then have their metavariables instantiated before the equality check. Their types are unified (using isDefEqGuarded) before synthetic metavariables are processed, which helps with default instance handling.

                                                                  Equations
                                                                    Instances For

                                                                      Tactic to check that the target agrees with a given expression.

                                                                      • guard_target = e checks that the target is defeq at reducible transparency to e.
                                                                      • guard_target =~ e checks that the target is defeq at default transparency to e.
                                                                      • guard_target =ₛ e checks that the target is syntactically equal to e.
                                                                      • guard_target =ₐ e checks that the target is alpha-equivalent to e.

                                                                      The term e is elaborated with the type of the goal as the expected type, which is mostly useful within conv mode.

                                                                      Equations
                                                                        Instances For

                                                                          Tactic to check that the target agrees with a given expression.

                                                                          • guard_target = e checks that the target is defeq at reducible transparency to e.
                                                                          • guard_target =~ e checks that the target is defeq at default transparency to e.
                                                                          • guard_target =ₛ e checks that the target is syntactically equal to e.
                                                                          • guard_target =ₐ e checks that the target is alpha-equivalent to e.

                                                                          The term e is elaborated with the type of the goal as the expected type, which is mostly useful within conv mode.

                                                                          Equations
                                                                            Instances For

                                                                              Tactic to check that a named hypothesis has a given type and/or value.

                                                                              • guard_hyp h : t checks the type up to reducible defeq,
                                                                              • guard_hyp h :~ t checks the type up to default defeq,
                                                                              • guard_hyp h :ₛ t checks the type up to syntactic equality,
                                                                              • guard_hyp h :ₐ t checks the type up to alpha equality.
                                                                              • guard_hyp h := v checks value up to reducible defeq,
                                                                              • guard_hyp h :=~ v checks value up to default defeq,
                                                                              • guard_hyp h :=ₛ v checks value up to syntactic equality,
                                                                              • guard_hyp h :=ₐ v checks the value up to alpha equality.

                                                                              The value v is elaborated using the type of h as the expected type.

                                                                              Equations
                                                                                Instances For

                                                                                  Tactic to check that a named hypothesis has a given type and/or value.

                                                                                  • guard_hyp h : t checks the type up to reducible defeq,
                                                                                  • guard_hyp h :~ t checks the type up to default defeq,
                                                                                  • guard_hyp h :ₛ t checks the type up to syntactic equality,
                                                                                  • guard_hyp h :ₐ t checks the type up to alpha equality.
                                                                                  • guard_hyp h := v checks value up to reducible defeq,
                                                                                  • guard_hyp h :=~ v checks value up to default defeq,
                                                                                  • guard_hyp h :=ₛ v checks value up to syntactic equality,
                                                                                  • guard_hyp h :=ₐ v checks the value up to alpha equality.

                                                                                  The value v is elaborated using the type of h as the expected type.

                                                                                  Equations
                                                                                    Instances For

                                                                                      Command to check equality of two expressions.

                                                                                      • #guard_expr e = e' checks that e and e' are defeq at reducible transparency.
                                                                                      • #guard_expr e =~ e' checks that e and e' are defeq at default transparency.
                                                                                      • #guard_expr e =ₛ e' checks that e and e' are syntactically equal.
                                                                                      • #guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

                                                                                      This is a command version of the guard_expr tactic.

                                                                                      Equations
                                                                                        Instances For

                                                                                          Command to check that an expression evaluates to true.

                                                                                          #guard e elaborates e ensuring its type is Bool then evaluates e and checks that the result is true. The term is elaborated without variables declared using variable, since these cannot be evaluated.

                                                                                          Since this makes use of coercions, so long as a proposition p is decidable, one can write #guard p rather than #guard decide p. A consequence to this is that if there is decidable equality one can write #guard a = b. Note that this is not exactly the same as checking if a and b evaluate to the same thing since it uses the DecidableEq instance to do the evaluation.

                                                                                          Note: this uses the untrusted evaluator, so #guard passing is not a proof that the expression equals true.

                                                                                          Equations
                                                                                            Instances For