Mercurial > cpdt > repo

comparison src/Subset.v @ 74:a21447f76aad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Break into Parts
author Adam Chlipala <adamc@hcoop.net>
date Fri, 03 Oct 2008 14:29:21 -0400
parents 535e1cd17d9a
children ec2c1830a7a1
comparison
equal deleted inserted replaced
73:535e1cd17d9a 74:a21447f76aad
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
19 (** %\chapter{Subset Types and Variations}% *) 19 (** %\part{Programming with Dependent Types}
20
21 \chapter{Subset Types and Variations}% *)
20 22
21 (** So far, we have seen many examples of what we might call "classical program verification." We write programs, write their specifications, and then prove that the programs satisfy their specifications. The programs that we have written in Coq have been normal functional programs that we could just as well have written in Haskell or ML. In this chapter, we start investigating uses of %\textit{%#<i>#dependent types#</i>#%}% to integrate programming, specification, and proving into a single phase. *) 23 (** So far, we have seen many examples of what we might call "classical program verification." We write programs, write their specifications, and then prove that the programs satisfy their specifications. The programs that we have written in Coq have been normal functional programs that we could just as well have written in Haskell or ML. In this chapter, we start investigating uses of %\textit{%#<i>#dependent types#</i>#%}% to integrate programming, specification, and proving into a single phase. *)
22 24
23 25
24 (** * Introducing Subset Types *) 26 (** * Introducing Subset Types *)
567 569
568 Eval simpl in typeCheck (Nat 0). 570 Eval simpl in typeCheck (Nat 0).
569 Eval simpl in typeCheck (Plus (Nat 1) (Nat 2)). 571 Eval simpl in typeCheck (Plus (Nat 1) (Nat 2)).
570 Eval simpl in typeCheck (Plus (Nat 1) (Bool false)). 572 Eval simpl in typeCheck (Plus (Nat 1) (Bool false)).
571 573
572 Print sumor.
573
574
575
576 Notation "e1 ;;; e2" := (if e1 then e2 else !!) 574 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
577 (right associativity, at level 60). 575 (right associativity, at level 60).
578 576
579 Theorem hasType_det : forall e t1, 577 Theorem hasType_det : forall e t1,
580 hasType e t1 578 hasType e t1