依值型別編程 / Dependently Typed Programming

Outline

Some compatibility problems

If you happened to have an earlier version of Agda installed, you may need to put the following derivatives into your program file:

{-# BUILTIN ZERO zero  #-}
{-# BUILTIN SUC  suc   #-}

infixl 6 _⊔_
postulate
  Level : Set
  lzero  : Level
  lsuc   : Level → Level
  _⊔_   : Level → Level → Level
{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero  #-}
{-# BUILTIN LEVELSUC  lsuc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}
zh-tw/dtp.txt · 上一次變更: 2014/07/04 21:22 由 scm
CC Attribution-Share Alike 3.0 Unported
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0