21 lines
486 B
Idris
21 lines
486 B
Idris
module Inductive
|
|
|
|
import Data.Vect
|
|
|
|
import Term
|
|
import Misc
|
|
|
|
{-
|
|
The type of a constructor, indexed like terms
|
|
-}
|
|
Constructor : (ctx : Index) -> (tags : Vect n Nat) -> Type
|
|
Constructor = Term ctx tags
|
|
|
|
{-
|
|
The type of an inductive definition. It is a vector of constructors.
|
|
's indexed by the number of constructors as well as the indecies for terms.
|
|
-}
|
|
public export
|
|
Inductive : Nat -> Index -> Vect n Nat -> Type
|
|
Inductive cons ctx tags = Vect cons (Constructor ctx (cons :: tags))
|