[Agda] on "Dependently Typed.."

[James Chapman]

Dear Serge,

You can direct these and any future comments to me.

I am maintaing Ulf's tutorial now.

Regards,

James

On Nov 6, 2012, at 12:53 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> Maybe you should send these comments directly to Ulf...
> 
> On 05.11.12 6:27 PM, Serge D. Mechveliani wrote:
>> A few notes on  "Dependently Typed Programming in Agda" by Ulf Norell.
>> 
>> * 2.1.
>> ... type theory developed at Chalmers University ...
>> References ?
>> 
>> * 2.1.
>> ...
>> Functions over Bool can be defined by pattern matching in a for
>> Haskell programmers familiar way:
>> --? -->
>> ... in a way familiar to Haskell programmers:
>> 
>> 2.4.
>> ...
>> Absurd patterns
>> ---------------
>> ... name   the family of numbers
>> --typo-?-->
>> ... namely the family ...
>> 
>> Regards,
>> Sergei
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> 
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda