The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

In the reference manual, () is listed in the ltac syntax. The manual does not say what it does. The error message from running the following hints that it has type unit.

Goal False.
  Fail let x:=() in revert x.
Abort.

The manual says, "the evaluation yields either a term, an integer or a tactic," and I don't see how the unit type fits in that list. Of course the manual doesn't mention the type of context patterns or intro patterns either.

What is an ltac unit used for? I can't find any built in tactics that accept it as a parameter.

Ltac true := constr:(true).
Ltac false := constr:(false).

(* Does not work if test_expr fails with a level greater than 0 *)
Ltac would_succeed test_expr :=
  match goal with
  | _ =>
    match goal with
    | _ => test_expr; gfail 1
    | _ => false
    end
  | _ => true
  end.

(* Takes constr or uconstr *)
Local Tactic Notation "take_term" constr(x) := idtac.

Local Tactic Notation "take_int" int_or_var(x) := idtac.
Local Tactic Notation "take_intropattern" simple_intropattern(x) := idtac.

(* Does not work if test_expr has gfail in it *)
Ltac is_tactic test_expr := would_succeed ltac:(admit; test_expr).

Ltac is_term test_expr := would_succeed ltac:(take_term test_expr).
Ltac is_int test_expr := would_succeed ltac:(take_int test_expr).
Ltac is_intropattern test_expr := would_succeed ltac:(take_intropattern test_expr).
Ltac is_context test_expr := would_succeed ltac:(first [
    let T:=fresh "T" in evar (T:Type); let x:=context test_expr [ T ] in idtac |
    let T:=fresh "T" with a:=fresh "a" in evar (T:Type); evar (a:T); let x:=context test_expr [ a ] in idtac
  ]).

Goal nat * nat.
  let x:=f_equal in let b:=is_tactic x in
    match b with
    | true => idtac
    end.
  let x:=() in let b:=is_tactic x in
    match b with
    | false => idtac
    end.
  let x:=constr:(0) in let b:=is_term x in
    match b with
    | true => idtac
    end.
  let x:=() in let b:=is_term x in
    match b with
    | false => idtac
    end.
  let x:=0 in let b:=is_int x in
    match b with
    | true => idtac
    end.
  let x:=() in let b:=is_int x in
    match b with
    | false => idtac
    end.
  let x:=fresh "v" in let b:=is_intropattern x in
    match b with
    | true => idtac
    end.
  let x:=() in let b:=is_intropattern x in
    match b with
    | false => idtac
    end.
  match goal with
  | |- context c [ _ ] =>
    let b:=is_context c in
      match b with
      | true => idtac
      end
  end.
  let x:=() in let b:=is_context x in
    match b with
    | false => idtac
    end.
Abort.

The only use I can think of for it is in a function that takes a variable number of arguments, to terminate the list of arguments.

Ltac is_terminator expr :=
  let a:=is_tactic expr in
  let b:=is_term expr in
  let c:=is_int expr in
  let d:=is_intropattern expr in
  let e:=is_context expr in
  match true with
  | a => false
  | b => false
  | c => false
  | d => false
  | e => false
  | _ => true
  end.

Ltac count_args :=
  let rec count total arg :=
    match (is_terminator arg) with
    | true => total
    | false => count (S total)
    end in
  count 0.

Goal False.
  let x:=count_args 1 2 3 f_equal () in idtac x.
Abort.