Skip to content
This repository has been archived by the owner on Sep 5, 2022. It is now read-only.

dannypsnl/k

Repository files navigation

k

Test Coverage Status Documentation Note

Warning This is a developing project

K is a theorem prover based on Racket ecosystem, interact with Racket in useful way is the major purpose of the project.

Installation

  1. only want core language
    raco pkg install --auto k-core
  2. wants standard library
    raco pkg install --auto k-core
    raco pkg install --auto k-lib

Usage

NOTE: implicit parameter haven't implemented, the following is a bit pseudo code

(def (symm {A : Type} {x y : A}
           [P : (≡ x y)])
  : (≡ y x)
  [refl => refl])

(def (trans {A : Type}
            {x y z : A}
            [P1 : (≡ x y)]
            [P2 : (≡ y z)])
  : (≡ x z)
  [refl refl => refl])

For developer

The following commands might be helpful for your development

raco pkg install --auto ./k-core
raco pkg install --auto ./k-lib
raco pkg install --auto ./k-doc
raco pkg install --auto ./k-test
raco pkg install --auto ./k-example
# apply git config of the project
git config commit.template $(pwd)/.gitmessage