Skip to content

Commit

Permalink
Try update Aya and see if it's updated
Browse files Browse the repository at this point in the history
  • Loading branch information
utensil committed Oct 6, 2024
1 parent e8f1832 commit 3e85407
Showing 1 changed file with 16 additions and 0 deletions.
16 changes: 16 additions & 0 deletions aya/literate.aya.md
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,22 @@ example def infixl [+] (a n : Nat) : Nat elim a
def foo =>
```

```aya
prim I
prim coe (r s : I) (A : I → Type) : A r → A s
prim Path
variable A B : Type
def infix = (a b : A) ⇒ Path (\i ⇒ A) a b
open inductive Bool | true | false
def not Bool : Bool
| true ⇒ false
| false ⇒ true
def id (x : Bool) ⇒ x
def Goal ⇒ id = (fn x ⇒ not (not x))
```

## Math formulas

$$
Expand Down

0 comments on commit 3e85407

Please sign in to comment.