The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

The one use I've found for () is as a dummy arg for a thunk, used to 
prevent early evaluation of certain overly-greedy Ltac forms, mostly 
matches:

Goal True.
let f := match goal with _ => idtac "goodbye" end in
idtac "hello"; f. (*prints "goodbye" then "hello"*)
Abort.

Goal True.
let f _ := match goal with _ => idtac "goodbye" end in
idtac "hello"; f (). (*prints "hello" then "goodbye"*)
Abort.

Obviously, anything will work in place of that () - but by using (), one 
signals what one is doing more clearly, precisely because there is no 
other use for ().

Also note that, if PMP gets his way in Ltac2, thunks will be required 
for such cases.

-- Jonathan


On 09/29/2016 04:22 AM, Kyle Stemen wrote:
> 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.