Sit alternatives and similar packages
Based on the "Dependent Types" category.
Alternatively, view Sit alternatives based on common mentions on social networks and blogs.

Agda
Agda is a dependently typed programming language / interactive theorem prover. 
agdasnippets
Library and tool to render the snippets in literate Agda files to hyperlinked HTML, leaving the rest of the text untouched.
Static code analysis for 29 languages.
Do you think we are missing an alternative of Sit or a related project?
Popular Comparisons
README
Sit: sizeirrelevant types
A prototype dependentlytyped language with sized natural numbers
Sit parses and typechecks .agda
that conform to the Sit language syntax.
Syntax (excerpt):
 Lexical stuff
 Single line comment
{ Block comment }
;  End of declaration (mandatory)
f_x'1  identifiers start with a letter, then have letters, digits, _ and '
 Declarations
x : T ;  type signature
x = t ;  definition
open import M ;  ignored, for Agda compatibility
 Sit specifics
oo  infinity size
i + 1  successor size
Nat a  type of natural numbers below size a
zero a  number zero (a is size annotation)
suc a n  successor of n (a is size annotation)
forall .i > T  irrelevant size quantification
forall ..i > T  relevant size quantification
fix T t n  recursive function over natural numbers
 T: return type
 t: functional
 n: natural number argument
\{ (zero _) > t; (suc _ x) > u }  case distinction function
 Inherited Agda syntax
U > T  nondependent function type
(x y z : U) > T  dependent function type
\ x y z > t  lambdaabstraction
t u  application
Set  first universe
Set1  second universe
Set a  universe of level a
Limitations
Sit only understands a tiny subset of the Agda language.
Sit does not understand layout, instead each declaration has to be terminated with
comment ;
.
Installation
Requires GHC and cabal, for instance via the Haskell Platform. In a shell, type
cabal install
Test
In a shell, type
Sit.bin test/Test.agda
Example
This is the addition function in Sit:
 Addition of natural numbers
plus : forall .i > Nat i > Nat oo > Nat oo ;
plus = \ i x y >
fix (\ i x > Nat oo)
(\ _ f > \
{ (zero _) > y
; (suc _ x) > suc oo (f x)
})
x