Some ATS codes for old version of "software foundations" book

Google Group
1

However, I think pattern match is better than “sif”…
How to use “case” for this?

There is an scase keyword in ATS, but I can’t tell more, as I never used
it yet.

2

When Ev_0 is used as a pattern, you need to write Ev_0().
The following code typechecks:

primplement ev_minus2 (e) =
case+ e of
| Ev_SS (Ev_0()) => Ev_0
| Ev_SS m =>> mOn Monday, May 18, 2015 at 5:04:00 AM UTC-4, Kiwamu Okabe wrote:

Hi all,

I read following article of BLUISH CODER.

Constructing Proofs with dataprop in ATS

Then, I understand rewriting Coq code with ATS is good exercise for
ATS/LF.
Following is some ATS codes for old version of “software foundations”
book.

https://github.com/jats-ug/practice-ats/blob/master/atslf_day/main.dats

However I can’t answer it.

extern prfun ev_minus2 {n:nat | n >= 2} (Ev n):<> Ev (n-2)

Following implementation causes a compile error.

$ vi main.dats 
primplement ev_minus2 (e) = 
  case+ e of 
  | Ev_SS Ev_0 => Ev_0 
  | Ev_SS m =>> ev_minus2 m 
$ patsopt -tc -d main.dats 
/home/kiwamu/src/practice-ats/atslf_day/main.dats: 4059(line=190, 
offs=5) -- 4082(line=190, offs=28): error(3): this pattern match 
clause is redundant.

How to fix it?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

3

You can just write:

primplement ev_minus2 (e) = case+ Ev_SS(m) => mOn Monday, May 18, 2015 at 11:23:36 AM UTC-4, gmhwxi wrote:

When Ev_0 is used as a pattern, you need to write Ev_0().
The following code typechecks:

primplement ev_minus2 (e) =
case+ e of
| Ev_SS (Ev_0()) => Ev_0
| Ev_SS m =>> m

On Monday, May 18, 2015 at 5:04:00 AM UTC-4, Kiwamu Okabe wrote:

Hi all,

I read following article of BLUISH CODER.

Constructing Proofs with dataprop in ATS

Then, I understand rewriting Coq code with ATS is good exercise for
ATS/LF.
Following is some ATS codes for old version of “software foundations”
book.

https://github.com/jats-ug/practice-ats/blob/master/atslf_day/main.dats

However I can’t answer it.

extern prfun ev_minus2 {n:nat | n >= 2} (Ev n):<> Ev (n-2)

Following implementation causes a compile error.

$ vi main.dats 
primplement ev_minus2 (e) = 
  case+ e of 
  | Ev_SS Ev_0 => Ev_0 
  | Ev_SS m =>> ev_minus2 m 
$ patsopt -tc -d main.dats 
/home/kiwamu/src/practice-ats/atslf_day/main.dats: 4059(line=190, 
offs=5) -- 4082(line=190, offs=28): error(3): this pattern match 
clause is redundant.

How to fix it?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN