GitHub - VictorTaelin/nanoproof · GitHub
/" data-turbo-transient="true" />
Skip to content
Search or jump to...
Search code, repositories, users, issues, pull requests...
-->
Search
Clear
Search syntax tips
Provide feedback
--><br>We read every piece of feedback, and take your input very seriously.
Include my email address so I can be contacted
Cancel
Submit feedback
Saved searches
Use saved searches to filter your results more quickly
-->
Name
Query
To see all available qualifiers, see our documentation.
Cancel
Create saved search
Sign in
/;ref_cta:Sign up;ref_loc:header logged out"}"<br>Sign up
Appearance settings
Resetting focus
You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.
Dismiss alert
{{ message }}
VictorTaelin
nanoproof
Public
Notifications<br>You must be signed in to change notification settings
Fork
Star<br>24
main
BranchesTags
Go to file
CodeOpen more actions menu
Folders and files<br>NameNameLast commit message<br>Last commit date<br>Latest commit
History<br>12 Commits<br>12 Commits
demo
demo
.gitignore
.gitignore
README.md
README.md
nanoproof.hs
nanoproof.hs
View all files
Repository files navigation
NanoProof
NanoProof is a tiny dependently typed proof checker in one Haskell file.
It supports:
a single universe, *
Pi, Sigma, equality, empty, unit, bit, and fixpoint types
lambdas, pairs, pattern eliminators, recursive values, and local lets
{==} reflexivity proofs
%proof; body equality rewriting
first-class guarded reduction views used consistently by printing, rewriting,<br>and equality
NanoProof intentionally has no termination checker. Recursive definitions and<br>fixpoints are accepted as written, so users are responsible for keeping them<br>terminating or productive.
Install
ghc -O2 nanoproof.hs -o nanoproof<br>cp nanoproof ~/.local/bin/nanoproof
Make sure ~/.local/bin is on PATH.
Usage
Check a file:
nanoproof demo/mul_comm.npf
If the file defines @main, NanoProof prints its normalized value after the<br>file checks.
Demo
demo/mul_comm.npf contains a Peano natural-number development and proves:
@mul_comm<br>: ∀@Nat. λa. ∀@Nat. λb.<br>{((@mul a) b) = ((@mul b) a) : @Nat}
The demo’s @main instantiates this theorem at 2 and 3.
Syntax
Comments:
// line comment
Definitions:
@name : type = term;
Core forms:
reduct guarded reduction view">* type of types<br>@name top-level reference<br>!x = value; body local let<br>$x. body guarded recursive value<br>μx. body fixpoint<br>∀A. F Pi over an explicit family<br>λx. body lambda<br>(f x) application<br>ΣA. F Sigma over an explicit family<br>#(a,b) pair<br>~f pair eliminator<br>⊥ empty type<br>λ{} empty eliminator<br>⊤ unit type<br>() unit value<br>λ() body unit eliminator<br>𝔹 bit type<br>0 / 1 bit values<br>λ{0: a; 1: b;} bit eliminator<br>{a = b : T} equality type<br>{==} reflexivity proof<br>%proof; body rewrite with an equality proof<br>↓source ~> reduct guarded reduction view
Function application is binary and prefix:
((@mul x) y)
Pi and Sigma codomains are ordinary families. Constant codomains are written by<br>returning the constant from a lambda:
∀@Nat. λx. @Nat<br>Σ@Nat. λx. @Nat
About<br>No description, website, or topics provided.<br>Resources<br>Readme<br>Activity<br>Stars<br>24 stars<br>Watchers<br>0 watching<br>Forks<br>1 fork<br>Report repository
Releases
Packages
Contributors
Languages
You can’t perform that action at this time.