Skip to content
/ kwed Public

minimalist proof assistant based on the Calculus of Inductive Constructions

License

Notifications You must be signed in to change notification settings

jacobhenn/kwed

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

28 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

kwed

kwed (/kwɛd/) is a minimal type-theoretic proof assistant based on the Calculus of Inductive Constructions.

kwed does not use tactics; all proofs are pure expressions not unlike in Agda.

kwed strives to avoid compiler builtins in favor of user-defined functionality. the set of built-in types is as minimal as possible, and you can easily see how anything in the standard library is defined by looking at its source code.

some standout features of kwed include:

  • painless module and import system
    • Rust-like import trees: use { Super.{Map, False.Not} }
  • optionally provide trailing named arguments: func a b (c: d, e: f)
  • non-headache-inducing anonymous function syntax, featuring terse parameter repitition: [x y: A, z: B] f x y z
  • structs (struct Pair(A B: Type) { first: A, second: B }) that desugar to inductive definitions with auto-generated field accessors
  • parametric induction:
    inductive IsEven: ℕ → Type { 
        0-is-even: IsEven 0, 
        plus-2-is-even: (n: ℕ, IsEven n) → IsEven (suc (suc n)),
    }
    

examples

natural number addition

the following kwed code defines the natural numbers () and addition of natural numbers (ℕ.+).

inductive ℕ: Type {
    0: ℕ,
    suc: ℕ → ℕ,
}

def +(x y: ℕ): ℕ {
    match y to [-] ℕ {            // define by induction on y
        0 => x,                   // in the case that y=0, return x
        suc y' => ℕ.suc (rec y'), // in the case that y=y'+1, return (x+y')+1 recursively
    }
}

standard library

for more advanced examples, feel free to browse the standard library.

About

minimalist proof assistant based on the Calculus of Inductive Constructions

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published