The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I've defined a couple simple types for untyped lambda calculus and SKI combinator calculus expressions:

Inductive lambda_expr : Set :=

| LVar : nat -> lambda_expr

| Lambda : lambda_expr -> lambda_expr

| LAppl : lambda_expr -> lambda_expr ->

    lambda_expr.

Coercion LAppl : lambda_expr >-> Funclass.

Inductive SKI_expr : Set :=

| SKIVar : nat -> SKI_expr

| S : SKI_expr

| K : SKI_expr

| I : SKI_expr

| SKIAppl : SKI_expr -> SKI_expr -> SKI_expr.

Coercion SKIAppl : SKI_expr >-> Funclass.

A minor annoyance that I run into with these, is that if I print the expressions back out, they have some unnecessary parentheses.  For example:

Check (S (K S) K).

==> (S (K S)) K : SKI_expr

Is there some easy setting I'm missing that would have the pretty printer eliminate those parentheses?  (The output of lambda_to_SKI_expr conversion would already be unwieldy enough without that.)

-- 

Daniel Schepler