[Agda] on "Dependently Typed.."

[Andreas Abel]

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/