Code

[ new ] Perfect binary trees#1063

Code

Merged

gallais merged 15 commits intoidris-lang:masteridris-lang/Idris2:masterfrom gallais:ralgallais/Idris2:ralCopy head branch name to clipboardFeb 22, 2021

+577-16

Commits

Commits on Feb 11, 2021

• [ libs ] some preliminary work

  gallais

  committed
  f8e4d04

Commits on Feb 12, 2021

• [ new ] Data.Nat.Exponentiation

  gallais

  committed
  5713678

• [ lib ] more preliminary work

  gallais

  committed
  558baf2

• [ new ] Data.Tree.Perfect

  Show description for 0a6511f
  gallais

  committed
  0a6511f

• [ doc ] for some of the perfect tree functions

  gallais

  committed
  c89c81b

• [ more ] proofs about exponentiation

  gallais

  committed
  78c5535

• [ fix ] more of Nat's structures

  gallais

  committed
  327d2e4

• [ refactor ] using the newly introduced functions and proofs

  gallais

  committed
  42d79f0

• [ more ] Applicative instance for Tree n

  gallais

  committed
  3d9305c

Commits on Feb 14, 2021

• [ new ] binary numbers

  Show description for 604f0de
  gallais

  committed
  604f0de

• [ new ] Data.Vect.Binary

  gallais

  committed
  b8b4792

• [ more ] zero-th index

  gallais

  committed
  2eeb529

• [ more ] weaken Path

  gallais

  committed
  6cb2580

Commits on Feb 18, 2021

• [ fix ] (^) is usually right-associative

  gallais

  committed
  01942bf

• Revert "[ more ] weaken Path"

  Show description for 7665962
  gallais

  committed
  7665962