Commit f2f3da93 authored by Nuria Brede's avatar Nuria Brede
Browse files

Initial.

parent 538b91b1
> %default total
> %auto_implicits off
> %access public export
> data Sigma : (A : Type) -> (P : A -> Type) -> Type where
> MkSigma : {A : Type} -> .{P : A -> Type} -> (x : A) -> (pf : P x) -> Sigma A P
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment